Zulip Chat Archive

Stream: general

Topic: VSCode expanding folders


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.

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?

Kevin Buzzard (Feb 08 2019 at 20:27):

I always have precisely 1 folder open because of this

Kenny Lau (Feb 08 2019 at 20:28):

well I have 50 copies of mathlib

Kevin Buzzard (Feb 08 2019 at 20:29):

well maybe you should learn about branches ;-)

Kenny Lau (Feb 08 2019 at 20:29):

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

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

Kevin Buzzard (Feb 08 2019 at 20:30):

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

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

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.

Kenny Lau (Feb 08 2019 at 20:32):

sure but I have no idea how the VSCode extension works

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.

Kenny Lau (Apr 08 2019 at 13:15):

@Gabriel Ebner would you know about this?

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.

Kenny Lau (Apr 08 2019 at 13:16):

oh ok


Last updated: Dec 20 2023 at 11:08 UTC