From 167549de59a0008a8fcde46e8a937e6683e33efa Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 22 Nov 2019 07:56:06 -0800
Subject: [PATCH] chore: fix tests

---
 tests/bench/compile.sh           | 2 +-
 tests/compiler/test_single.sh    | 2 +-
 tests/lean/fail/test_single.sh   | 2 +-
 tests/lean/run/test_single.sh    | 2 +-
 tests/lean/test_single.sh        | 2 +-
 tests/lean/trust0/test_single.sh | 2 +-
 6 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/tests/bench/compile.sh b/tests/bench/compile.sh
index e8080811f7..18d5b7e0b6 100755
--- a/tests/bench/compile.sh
+++ b/tests/bench/compile.sh
@@ -6,7 +6,7 @@ fi
 ulimit -s 8192
 BIN_DIR=../../bin
 LEAN=$BIN_DIR/lean
-export LEAN_PATH=Init=../../library/Init:Test=.
+export LEAN_PATH=Init=../../src/Init:Test=.
 ff=$1
 
 if [[ "$OSTYPE" == "msys" ]]; then
diff --git a/tests/compiler/test_single.sh b/tests/compiler/test_single.sh
index 92978f5f6a..91d42d341e 100755
--- a/tests/compiler/test_single.sh
+++ b/tests/compiler/test_single.sh
@@ -6,7 +6,7 @@ fi
 ulimit -s 8192
 LEAN=$1
 BIN_DIR=../../bin
-export LEAN_PATH=Init=../../library/Init:Test=.
+export LEAN_PATH=Init=../../src/Init:Test=.
 if [ $# -ne 3 ]; then
     INTERACTIVE=no
 else
diff --git a/tests/lean/fail/test_single.sh b/tests/lean/fail/test_single.sh
index 4ebd0ce30f..9fb87b2f91 100644
--- a/tests/lean/fail/test_single.sh
+++ b/tests/lean/fail/test_single.sh
@@ -5,7 +5,7 @@ if [ $# -ne 2 ]; then
 fi
 ulimit -s 8192
 LEAN=$1
-export LEAN_PATH=Init=../../../library/Init:Test=.
+export LEAN_PATH=Init=../../../src/Init:Test=.
 f=$2
 echo "-- testing $f"
 "$LEAN" -j 0 "$f"
diff --git a/tests/lean/run/test_single.sh b/tests/lean/run/test_single.sh
index 7c4ddc4209..66935dbdbf 100755
--- a/tests/lean/run/test_single.sh
+++ b/tests/lean/run/test_single.sh
@@ -5,7 +5,7 @@ if [ $# -ne 2 ]; then
 fi
 ulimit -s 8192
 LEAN=$1
-export LEAN_PATH=Init=../../../library/Init:Test=.
+export LEAN_PATH=Init=../../../src/Init:Test=.
 f=$2
 echo "-- testing $f"
 "$LEAN" -j 0 "$f"
diff --git a/tests/lean/test_single.sh b/tests/lean/test_single.sh
index e8a36ee7be..344ec25b42 100755
--- a/tests/lean/test_single.sh
+++ b/tests/lean/test_single.sh
@@ -5,7 +5,7 @@ if [ $# -ne 3 -a $# -ne 2 ]; then
 fi
 ulimit -s 8192
 LEAN=$1
-export LEAN_PATH=Init=../../library/Init:Test=.
+export LEAN_PATH=Init=../../src/Init:Test=.
 if [ $# -ne 3 ]; then
     INTERACTIVE=no
 else
diff --git a/tests/lean/trust0/test_single.sh b/tests/lean/trust0/test_single.sh
index bb6c511258..5b74e24046 100755
--- a/tests/lean/trust0/test_single.sh
+++ b/tests/lean/trust0/test_single.sh
@@ -5,7 +5,7 @@ if [ $# -lt 2 ]; then
 fi
 ulimit -s 8192
 LEAN=$1
-export LEAN_PATH=Init=../../../library/Init:Test=.
+export LEAN_PATH=Init=../../../src/Init:Test=.
 f=$2
 shift 2
 echo "-- testing $f"