diff --git a/tests/compiler/test_single_interpret.sh b/tests/compiler/test_single_interpret.sh index 1a6a83f1a7..2f591b8cf0 100755 --- a/tests/compiler/test_single_interpret.sh +++ b/tests/compiler/test_single_interpret.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/ctor_layout.lean b/tests/lean/ctor_layout.lean index cabd1e478d..1ac357fc1b 100644 --- a/tests/lean/ctor_layout.lean +++ b/tests/lean/ctor_layout.lean @@ -3,7 +3,7 @@ open Lean open Lean.IR def tst : IO Unit := -do initSearchPath "Init=../../library/Init"; +do initSearchPath "Init=../../src/Init"; env ← importModules [{module := `Init.Lean.Compiler.IR.Basic}]; ctorLayout ← IO.ofExcept $ getCtorLayout env `Lean.IR.Expr.reuse; ctorLayout.fieldInfo.forM $ fun finfo => IO.println (format finfo); diff --git a/tests/plugin/test_single.sh b/tests/plugin/test_single.sh index c3e0812584..6b0216220a 100755 --- a/tests/plugin/test_single.sh +++ b/tests/plugin/test_single.sh @@ -5,7 +5,7 @@ if [ $# -ne 2 -a $# -ne 1 ]; then fi ulimit -s 8192 BIN_DIR=../../bin -export LEAN_PATH=Init=../../library/Init:Test=. +export LEAN_PATH=Init=../../src/Init:Test=. if [ $# -ne 2 ]; then INTERACTIVE=no else