max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: skip elan test if no elan found

Browse source
This commit is contained in:
Sebastian Ullrich 2022-07-08 23:12:11 +02:00 • committed by Mac
parent 49a025889a
commit b57ca74794
1 changed files with 3 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
test/62/test.sh
View file

@ -1,6 +1,9 @@
#!/usr/bin/env bash
set -euxo pipefail
# skip if no elan found
command -v elan > /dev/null || (echo "elan not found; skipping test"; exit 0)
./clean.sh
lake +leanprover/lean4:4.0.0-m3 new foo
cd foo