Rebuilding dependent files in vs code

Stream: general

[Ruben Van de Velde]

For the last few days, vs code seems to actually be rebuilding dependent files that don't have oleans without requiring ctrl-shift-x - has anyone else noticed that or did I mess something up in my setup? (and if the latter, any idea what it might be?)

[Marc Huisinga]

Thanks for the report. I just noticed that this is something I broke in vscode-lean4 when releasing 0.0.156. I'll fix it in a second.

[Marc Huisinga]

This is now fixed in 0.0.159.

[Ruben Van de Velde]

Thanks!