Also run fstar tests which are symlinks

viperproject · Dec 27, 2024 · f4c6a8a · f4c6a8a
1 parent a763fb2
commit f4c6a8a
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/fstar/tests.sh b/fstar/tests.sh
@@ -1,2 +1,2 @@
 TESTS="$(realpath "$(dirname "$0")")/fstar/tests"
-find "$TESTS" -name "Makefile" -type f
+find -L "$TESTS" -name "Makefile" -type f