lean4-htt/examples/precompile/test.sh
2022-11-23 20:56:40 -05:00

8 lines
126 B
Bash
Executable file

set -ex
LAKE=${LAKE:-../../build/bin/lake}
./clean.sh
$LAKE -d bar update
$LAKE -d bar build # tests #83
$LAKE -d foo build