diff --git a/tests/lean/test.sh b/tests/lean/test.sh index f94632525..21a4b5b75 100755 --- a/tests/lean/test.sh +++ b/tests/lean/test.sh @@ -3,6 +3,7 @@ if [ $# -ne 2 -a $# -ne 1 ]; then echo "Usage: test.sh [lean-executable-path] [yes/no]?" exit 1 fi +ulimit -s unlimited LEAN=$1 if [ $# -ne 2 ]; then INTERACTIVE=no