klab fetch shouldn't focus

[asymmetric]

Or at least, it should make it possible not to focus.

The usecase is me trying to debug two proofs, and fetch stealing the focus away from the currently focused one seems unnecessary.

[d-xo]

I quite like fetch focusing, I would for sure keep it as the default.

You can also fetch into a new directory (e.g. cd $(mktemp -d) && klab fetch <URL>), and everything works fine without messing up the focused proof in your current directory.

[asymmetric]

Yeah that's true. I just think it's a behaviour that isn't necessarily part of the semantics of a "fetch".

[asymmetric]

Alternatively, since it asks questions already, it could ask if it should focus and default to yes.

[d-xo]

Alternatively, since it asks questions already, it could ask if it should focus and default to yes.

I would be OK with this 👍 👌