Telling what lean is currently building (vs code)

Stream: new members

[Eric Wieser]

I'm editing files in mathlib, and finding that the orange "busy" bar spans my entire file for a very long time.

This presumably means that lean is rebuilding a dependent file in the background. Is there any way for me to find out which one?

[Kenny Lau]

well you can do lean --make [current file] in terminal

[Kenny Lau]

and look at the output