aboutsummaryrefslogtreecommitdiff
path: root/dev/dune-dbg.in
diff options
context:
space:
mode:
authorGaëtan Gilbert2018-11-08 15:01:24 +0100
committerGaëtan Gilbert2018-11-08 15:01:24 +0100
commita7522a0ea76a6efaed9342d08a95363b56d88d32 (patch)
tree9ab8bd176949a072e0edb1f79502142cedcdb0b2 /dev/dune-dbg.in
parent108c15b51a7d5f647c8681fe7a37c86f0c5a8b9c (diff)
Remove checker printers
Now that the checker is using the regular kernel files it can also use the normal printers.
Diffstat (limited to 'dev/dune-dbg.in')
-rwxr-xr-xdev/dune-dbg.in14
1 files changed, 8 insertions, 6 deletions
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