Build scripts do not exit after a standalone command fails

[PEliet]

The comments in both build.sh and build-web.sh say that the scripts stop when any command fails:

set -o pipefail # stop if any command fails

However, pipefail only changes the exit status of pipelines. It does not make Bash exit after a standalone command fails. For example, if lake exe cache get fails, the script may still continue to the later build commands.

Would you accept a small PR that changes both scripts to:
set -e -o pipefail # stop if a command or pipeline fails

This would only modify build.sh and build-web.sh; it would not change Lean source files, proofs, or dependencies.

[Chessing234]

Fix in #590.

[Chessing234]

CI failed on runner disk space (not the patch). Retrying.

[Chessing234]

CI green on #590.

[Chessing234]

Also opened #594 / #595 for doc label and --/ closer typos found while reviewing.

[Chessing234]

Fixed by #589 (set -e in build.sh / build-web.sh).

[Chessing234]

This looks fixed on main already by #589 (set -e in both build scripts).

[Chessing234]

Already fixed on main by #589 (set -e in both build scripts).

[Chessing234]

This was fixed in #589 (set -e -o pipefail is on main now).

[Chessing234]

Fixed on main by #589 (set -e -o pipefail in both build scripts).

[Chessing234]

Closing as fixed on main by #589 (set -e -o pipefail is present in both build.sh and build-web.sh).

[Chessing234]

This is fixed on main by #589 — both build.sh and build-web.sh now have set -e -o pipefail. Happy for a maintainer to close.

[Chessing234]

already fixed on main by #589 (set -e -o pipefail in both build scripts). happy for a maintainer to close.

[Chessing234]

Closing: fixed on main by #589 (set -e -o pipefail in build.sh and build-web.sh).