From 9ebf44d84754adc5b64fcf612c6816c02c80462d Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 2 Feb 2019 19:29:23 -0500 Subject: Imported Upstream version 8.9.0 --- test-suite/misc/deps-order.sh | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) (limited to 'test-suite/misc/deps-order.sh') diff --git a/test-suite/misc/deps-order.sh b/test-suite/misc/deps-order.sh index 299f4946..6bb2ba2d 100755 --- a/test-suite/misc/deps-order.sh +++ b/test-suite/misc/deps-order.sh @@ -1,17 +1,18 @@ +#!/bin/sh # 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/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 --strip-trailing-cr misc/deps/deps.out $tmpoutput 2>&1 +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 --strip-trailing-cr misc/deps/deps.out "$tmpoutput" 2>&1 R=$? times $coqc -R misc/deps/lib lib misc/deps/lib/foo.v 2>&1 $coqc -R misc/deps/lib lib -R misc/deps/client client misc/deps/client/foo.v 2>&1 $coqtop -R misc/deps/lib lib -R misc/deps/client client -load-vernac-source misc/deps/client/bar.v 2>&1 S=$? -if [ $R = 0 -a $S = 0 ]; then +if [ $R = 0 ] && [ $S = 0 ]; then printf "coqdep and coqtop agree\n" exit 0 else -- cgit v1.2.3