From cdceb6ac279196b04d3276cccdbbfce88bec2e4c Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 11 Jun 2017 11:27:01 +0200
Subject: Fixing base_include after loc is an option (30d3515).

---
 dev/base_include | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/dev/base_include b/dev/base_include
index defea713d8..f9af0696b1 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -233,7 +233,7 @@ let pf_e gl s =
 let _ = Flags.in_debugger := false
 let _ = Flags.in_toplevel := true
 let _ = Constrextern.set_extern_reference
-  (fun loc _ r -> Libnames.Qualid (loc,Nametab.shortest_qualid_of_global Idset.empty r));;
+  (fun ?loc _ r -> Libnames.Qualid (loc,Nametab.shortest_qualid_of_global Idset.empty r));;
 
 open Coqloop
 let go = loop
-- 
cgit v1.2.3


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(-)

diff --git a/test-suite/misc/printers.sh b/test-suite/misc/printers.sh
index c822d0eb37..28e7dc362f 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