aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/misc/printers.sh
blob: 28e7dc362f942c144a4a3260c96fb28c2b833a9a (plain)
1
2
3
printf "Drop. #use\"include\";; #quit;;\n" | $coqtopbyte 2>&1 | egrep "Error|Unbound"
if [ $? = 0 ]; then exit 1; else exit 0; fi