From a7522a0ea76a6efaed9342d08a95363b56d88d32 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 8 Nov 2018 15:01:24 +0100
Subject: Remove checker printers

Now that the checker is using the regular kernel files it can also use
the normal printers.
---
 dev/dune-dbg.in | 14 ++++++++------
 1 file changed, 8 insertions(+), 6 deletions(-)

(limited to 'dev/dune-dbg.in')

diff --git a/dev/dune-dbg.in b/dev/dune-dbg.in
index 464e026400..3f3df23fe1 100755
--- a/dev/dune-dbg.in
+++ b/dev/dune-dbg.in
@@ -2,10 +2,12 @@
 
 # Run in a proper install dune env.
 case $1 in
-checker)
-  ocamldebug `ocamlfind query -recursive -i-format coq.checker_printers` -I +threads -I dev _build/default/checker/main.bc
-  ;;
-*)
-  ocamldebug `ocamlfind query -recursive -i-format coq.top_printers` -I +threads -I dev _build/default/topbin/coqtop_byte_bin.bc
-  ;;
+    checker)
+        exe=_build/default/checker/main.bc
+        ;;
+    *)
+        exe=_build/default/topbin/coqtop_byte_bin.bc
+        ;;
 esac
+
+ocamldebug $(ocamlfind query -recursive -i-format coq.top_printers) -I +threads -I dev $exe
-- 
cgit v1.2.3