## Stream: new members

### Topic: Telling what lean is currently building (vs code)

#### Eric Wieser (Jul 30 2020 at 10:26):

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 (Jul 30 2020 at 10:36):

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

#### Kenny Lau (Jul 30 2020 at 10:36):

and look at the output

Last updated: May 09 2021 at 19:11 UTC