diff options
Diffstat (limited to 'test-suite/misc/deps-order.sh')
-rwxr-xr-x | test-suite/misc/deps-order.sh | 2 |
1 files changed, 1 insertions, 1 deletions
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 |