Zulip Chat Archive

Stream: general

Topic: VSCode expanding folders


view this post on Zulip Kenny Lau (Feb 08 2019 at 19:21):

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.

view this post on Zulip Kevin Buzzard (Feb 08 2019 at 20:27):

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?

view this post on Zulip Kevin Buzzard (Feb 08 2019 at 20:27):

I always have precisely 1 folder open because of this

view this post on Zulip Kenny Lau (Feb 08 2019 at 20:28):

well I have 50 copies of mathlib

view this post on Zulip Kevin Buzzard (Feb 08 2019 at 20:29):

well maybe you should learn about branches ;-)

view this post on Zulip Kenny Lau (Feb 08 2019 at 20:29):

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

view this post on Zulip Kevin Buzzard (Feb 08 2019 at 20:29):

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

view this post on Zulip Kevin Buzzard (Feb 08 2019 at 20:30):

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

view this post on Zulip Kenny Lau (Feb 08 2019 at 20:30):

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

view this post on Zulip Kevin Buzzard (Feb 08 2019 at 20:31):

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.

view this post on Zulip Kenny Lau (Feb 08 2019 at 20:32):

sure but I have no idea how the VSCode extension works

view this post on Zulip Kenny Lau (Apr 08 2019 at 13:15):

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.

view this post on Zulip Kenny Lau (Apr 08 2019 at 13:15):

@Gabriel Ebner would you know about this?

view this post on Zulip Gabriel Ebner (Apr 08 2019 at 13:16):

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.

view this post on Zulip Kenny Lau (Apr 08 2019 at 13:16):

oh ok


Last updated: May 14 2021 at 05:20 UTC