diff options
| author | Gaëtan Gilbert | 2018-11-08 15:01:24 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-11-08 15:01:24 +0100 |
| commit | a7522a0ea76a6efaed9342d08a95363b56d88d32 (patch) | |
| tree | 9ab8bd176949a072e0edb1f79502142cedcdb0b2 /dev/dune-dbg.in | |
| parent | 108c15b51a7d5f647c8681fe7a37c86f0c5a8b9c (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-x | dev/dune-dbg.in | 14 |
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 |
