From e9c17b154c841626840d300ff954fcbaaa6d19ee Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 10 Jul 2014 23:26:55 +0100 Subject: [PATCH] fix(tests/lean): define LEAN_PATH in tests scripts Signed-off-by: Leonardo de Moura --- tests/lean/test.sh | 1 + tests/lean/test_single.sh | 1 + 2 files changed, 2 insertions(+) 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