From 7e0f61eb7cd16b2f2e58ce7ca18992fde7ac9aea Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 11 Jun 2017 11:34:11 +0200 Subject: A stronger test that #use"include";; works well. --- test-suite/misc/printers.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'test-suite/misc') diff --git a/test-suite/misc/printers.sh b/test-suite/misc/printers.sh index c822d0eb3..28e7dc362 100755 --- a/test-suite/misc/printers.sh +++ b/test-suite/misc/printers.sh @@ -1,3 +1,3 @@ -printf "Drop. #use\"include\";; #quit;;\n" | $coqtopbyte 2>&1 | grep Unbound +printf "Drop. #use\"include\";; #quit;;\n" | $coqtopbyte 2>&1 | egrep "Error|Unbound" if [ $? = 0 ]; then exit 1; else exit 0; fi -- cgit v1.2.3