Zulip Chat Archive

Stream: general

Topic: suppressing warnings in `leanpkg build`

Kevin Buzzard (Apr 21 2019 at 00:53):

How do I suppress warnings (or more specifically sorries, or importing a file with sorries) whilst running leanpkg build? I just want to check for errors.

Simon Hudon (Apr 21 2019 at 00:59):

I do leanpkg build | grep error

Kevin Buzzard (Apr 21 2019 at 01:00):

Fair do's

Last updated: Dec 20 2023 at 11:08 UTC