lean --make output on Windows

Stream: general

[Kevin Buzzard]

Trying to remotely debug a tooling issue on Windows with a beginner and I remember that lean --make path/to/file.lean just sits there producing no output whatsoever on Windows, whereas on linux I get continually updated about which file and line the lean binary is currently working on. Is this something which can now be fixed?

[Wojciech Nawrocki]

I'd observed this as well but thought it was just my mingw installation being weird. It should be fixable.