aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rwxr-xr-xtest-suite/misc/deps-checksum.sh2
-rwxr-xr-xtest-suite/misc/deps-order.sh2
2 files changed, 2 insertions, 2 deletions
diff --git a/test-suite/misc/deps-checksum.sh b/test-suite/misc/deps-checksum.sh
index 1e2afb754..e07612b84 100755
--- a/test-suite/misc/deps-checksum.sh
+++ b/test-suite/misc/deps-checksum.sh
@@ -1,4 +1,4 @@
-rm -f misc/deps/*/*.vo
+rm -f misc/deps/A/*.vo misc/deps/B/*.vo
$coqc -R misc/deps/A A misc/deps/A/A.v
$coqc -R misc/deps/B A misc/deps/B/A.v
$coqc -R misc/deps/B A misc/deps/B/B.v
diff --git a/test-suite/misc/deps-order.sh b/test-suite/misc/deps-order.sh
index 375b706f0..00c5eb1bd 100755
--- a/test-suite/misc/deps-order.sh
+++ b/test-suite/misc/deps-order.sh
@@ -1,7 +1,7 @@
# Check that both coqdep and coqtop/coqc supports -R
# Check that both coqdep and coqtop/coqc takes the later -R
# See bugs 2242, 2337, 2339
-rm -f misc/deps/*/*.vo
+rm -f misc/deps/lib/*.vo misc/deps/client/*.vo
tmpoutput=`mktemp /tmp/coqcheck.XXXXXX`
$coqdep -R misc/deps/lib lib -R misc/deps/client client misc/deps/client/bar.v 2>&1 | head -n 1 > $tmpoutput
diff -u misc/deps/deps.out $tmpoutput 2>&1