mathlib3
3c33aba3 - ci(.github/workflows/*): Make build step fail if lean returns nonzero value (#15520)

Commit
3 years ago
ci(.github/workflows/*): Make build step fail if lean returns nonzero value (#15520) Currently, when building mathlib, if the second `lean --make src` returns a nonzero value, say due to an out-of-memory error, this value will be masked by the pipe, causing the build step to appear to succeed. The problem will then show up down the line, say in linting. This bit us in lean-liquid. This change causes the build step to fail if the `lean --make` command fails.
Author
Parents
Loading