diff --git a/tests/lean/test.sh b/tests/lean/test.sh index 1001f8cee3..63a2f5c8be 100755 --- a/tests/lean/test.sh +++ b/tests/lean/test.sh @@ -5,6 +5,7 @@ if [ $# -ne 2 -a $# -ne 1 ]; then fi ulimit -s 8192 LEAN=$1 +export LEAN_PATH=../../library/standard:. if [ $# -ne 2 ]; then INTERACTIVE=no else diff --git a/tests/lean/test_single.sh b/tests/lean/test_single.sh index 5f66165120..2d1b73206e 100755 --- a/tests/lean/test_single.sh +++ b/tests/lean/test_single.sh @@ -5,6 +5,7 @@ if [ $# -ne 3 -a $# -ne 2 ]; then fi ulimit -s 8192 LEAN=$1 +export LEAN_PATH=../../library/standard:. if [ $# -ne 3 ]; then INTERACTIVE=no else