From 61926bbb32c2a91b93cb0e5f00cdd69cd4245e72 Mon Sep 17 00:00:00 2001 From: tydeu Date: Thu, 16 Jun 2022 02:24:46 -0400 Subject: [PATCH] chore: fix test --- test/75/test.sh | 1 + 1 file changed, 1 insertion(+) diff --git a/test/75/test.sh b/test/75/test.sh index d145a0e81e..941b9305c9 100755 --- a/test/75/test.sh +++ b/test/75/test.sh @@ -5,6 +5,7 @@ LAKE=${LAKE:-../../../build/bin/lake} cd foo rm -rf build +mkdir -p Foo echo $'def a := "a"' > Foo/Test.lean echo $'import Foo.Test def hello := a' > Foo.lean ${LAKE} build