lean4/tests/server/run_test.sh at master - lean4 - Gitea: Git with a cup of tea

sdgoij/lean4

mirror of https://github.com/leanprover/lean4.git synced 2026-03-17 18:34:06 +00:00

Files

Garmelon 6b7f0ad5fc chore: check test output before exit code in piles (#12947 )

This improves the feedback when tests fail. Getting a diff is more
useful than a vague exit code.

2026-03-17 16:34:21 +00:00

9 lines

127 B

Bash

Raw Permalink Blame History

 run_before "$1"
 capture_only "$1" \
   lean -Dlinter.all=false --run "$1"
 check_out_file
 check_exit_is_success
 run_after "$1"