From ab386983df210e0a7252da365cbdc829a482da58 Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Thu, 7 Dec 2023 04:21:31 +1100 Subject: [PATCH] chore: build all of Mathlib in Mathlib tests in case cache is not present --- test/Mathlib/test.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/test/Mathlib/test.sh b/test/Mathlib/test.sh index 6d7759b..0c5f998 100755 --- a/test/Mathlib/test.sh +++ b/test/Mathlib/test.sh @@ -5,7 +5,7 @@ IN_DIR="test" EXPECTED_DIR="test" lake exe cache get > /dev/null -lake build +lake build Mathlib # Iterate over each .in file in the test directory for infile in $IN_DIR/*.in; do