VSCode expanding folders

Stream: general

[Kenny Lau]

VSCode now expands all the root folders whenever I change them by a slightest bit. This is very inconvenient for people like me who have 20 folders open.

[Kevin Buzzard]

Did you know that if you just close some folders then when you re-open them they will be in exactly the same state as you left them?

[Kevin Buzzard]

I always have precisely 1 folder open because of this

[Kenny Lau]

well I have 50 copies of mathlib

[Kevin Buzzard]

well maybe you should learn about branches ;-)

[Kenny Lau]

I can do branches all right, my olean files can't

[Kevin Buzzard]

and even then my comment still remains -- just call the directories mathlib_thisbranch etc and open them one at a time

[Kevin Buzzard]

Whenever you open one it will be just as you left it

[Kenny Lau]

sure, but then a recent update caused all the root folders to expand whenever I move anything

[Kevin Buzzard]

OTOH if you were handling 10 open folders fine before, and now you aren't, then there's every change that you can just change something back.

[Kenny Lau]

sure but I have no idea how the VSCode extension works

[Kenny Lau]

VSCode now expands all the root folders whenever I change them by a slightest bit. This is very inconvenient for people like me who have 20 folders open.

Somehow VSCode stopped this behaviour. Thanks to whoever tweaked the code appropriately.

[Kenny Lau]

@Gabriel Ebner would you know about this?

[Gabriel Ebner]

No, I haven't heard of it. But I think this is a purely upstream issue. Our extension probably has nothing to do with it.

[Kenny Lau]

oh ok