lean4-htt/tests/bench/compile.sh
2022-12-30 12:45:30 +01:00

9 lines
189 B
Bash
Executable file

#!/usr/bin/env bash
source ../common.sh
compile_lean_c_backend
# Then check the LLVM version
if lean_has_llvm_support; then
echo "running LLVM program..."
compile_lean_llvm_backend
fi