a flag to stop `lean --make` at the first error

When I call lean --make I often don't care about the full output; either it succeeds, or there's an error, and I want to start fixing from the first error. Would it be possible to add a flag that would stop the build as soon as something goes wrong?

mathlib pipes the build into a Python script to short circuit on errors, and I'd like to duplicate that behavior in other CI in a less hackish way.

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
    • Specifically, check out the wishlist, open RFCs,
      or feature requests.
  • Reduced the issue to a self-contained, reproducible test case.

Description

[Description of the issue]

Steps to Reproduce

1. [First Step]
2. [Second Step]
3. [and so on...]

Expected behavior: [What you expect to happen]

Actual behavior: [What actually happens]

Reproduces how often: [What percentage of the time does it reproduce?]

Versions

You can get this information from copy and pasting the output of lean --version,
please include the OS and what version of the OS you're running.

Additional Information

Any additional information, configuration or data that might be necessary to reproduce the issue.

Start by locating the lean --make command entry point and compare its behavior with the mathlib Python script mentioned in the issue. Done means a supported flag stops the build at the first error, with the behavior verified for the command's failure path.