Zulip Chat Archive
Stream: general
Topic: Remove trace in lake build
SnO2WMaN (Jan 25 2026 at 06:40):
How to remove trace: .> LEAN_PATH=... in CLI output?
I tried lake build -q --log-level=error, still error and also trace outputs.
lake --version is Lake version 5.0.0-src+2fcce72 (Lean version 4.27.0-rc1)
Last updated: Feb 28 2026 at 14:05 UTC