lean4-htt/tests/docparse/run_test.sh
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

8 lines
258 B
Bash

# IO.Process.exit (used by the file worker) seems to be incompatible with LSAN
# TODO: investigate or work around
export ASAN_OPTIONS=detect_leaks=0
capture_only "$1" \
lean -Dlinter.all=false --run run_test.lean "$1"
check_out_file
check_exit_is_success