From 7f17e151c0a2666263d3854c064acdfea29edf53 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 8 May 2017 17:19:22 +0200
Subject: Adding tests for testing exit status and #use"include".

---
 test-suite/.csdp.cache                | Bin 89077 -> 89077 bytes
 test-suite/Makefile                   |  30 +++++++++++++++++++++++++++++-
 test-suite/misc/exitstatus/illtyped.v |   1 +
 3 files changed, 30 insertions(+), 1 deletion(-)
 create mode 100644 test-suite/misc/exitstatus/illtyped.v

diff --git a/test-suite/.csdp.cache b/test-suite/.csdp.cache
index ba85286dd3..b99d80e95f 100644
Binary files a/test-suite/.csdp.cache and b/test-suite/.csdp.cache differ
diff --git a/test-suite/Makefile b/test-suite/Makefile
index c10cd4ed44..779f5455ae 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -33,6 +33,7 @@ LIB := $(shell cd ..; pwd)
 coqtop := $(BIN)coqtop -boot -q -batch -test-mode -R prerequisite TestSuite
 bincoqc := $(BIN)coqc -coqlib $(LIB) -R prerequisite TestSuite
 bincoqchk := $(BIN)coqchk -coqlib $(LIB) -R prerequisite TestSuite
+coqtopbyte := $(BIN)coqtop.byte
 
 command := $(coqtop) -top Top -async-proofs-cache force -load-vernac-source
 coqc := $(coqtop) -compile
@@ -405,7 +406,7 @@ modules/%.vo: modules/%.v
 # Miscellaneous tests
 #######################################################################
 
-misc: misc/deps-order.log misc/universes.log misc/deps-checksum.log
+misc: misc/deps-order.log misc/universes.log misc/deps-checksum.log misc/printers.log misc/exitstatus.log
 
 # Check that both coqdep and coqtop/coqc supports -R
 # Check that both coqdep and coqtop/coqc takes the later -R
@@ -477,6 +478,33 @@ misc/universes.log: misc/universes/all_stdlib.v
 misc/universes/all_stdlib.v:
 	cd .. && $(MAKE) test-suite/$@
 
+misc/printers.log:
+	@echo "TEST      printers"
+	$(HIDE){ \
+	  echo $(call log_intro,$<); \
+	  printf "Drop. #use\"include\";; #quit;;" | $(coqtopbyte) 2>&1 | grep Unbound; R=$$?; times; \
+	  if [ $$R != 0 ]; then \
+	    echo $(log_success); \
+	    echo "    misc/printers...Ok"; \
+	  else \
+	    echo $(log_failure); \
+	    echo "    misc/printers...Error!"; \
+	  fi; \
+	} > "$@"
+
+misc/exitstatus.log:
+	@echo "TEST      exitstatus"
+	$(HIDE){ \
+	  echo $(call log_intro,$<); \
+	  $(coqc) misc/exitstatus/illtyped.v 2>&1; R=$$?; times; \
+	  if [ $$R != 0 ]; then \
+	    echo $(log_success); \
+	    echo "    misc/exitstatus...Ok"; \
+	  else \
+	    echo $(log_failure); \
+	    echo "    misc/exitstatus...Error!"; \
+	  fi; \
+	} > "$@"
 
 # IDE : some tests of backtracking for coqtop -ideslave
 
diff --git a/test-suite/misc/exitstatus/illtyped.v b/test-suite/misc/exitstatus/illtyped.v
new file mode 100644
index 0000000000..df6bbb389c
--- /dev/null
+++ b/test-suite/misc/exitstatus/illtyped.v
@@ -0,0 +1 @@
+Check S S.
-- 
cgit v1.2.3