diff options
Diffstat (limited to 'dev/dune-dbg.in')
| -rwxr-xr-x | dev/dune-dbg.in | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/dev/dune-dbg.in b/dev/dune-dbg.in index 80ad0500e0..bd0a837938 100755 --- a/dev/dune-dbg.in +++ b/dev/dune-dbg.in @@ -3,11 +3,14 @@ # Run in a proper install dune env. case $1 in checker) + shift exe=_build/default/checker/coqchk.bc ;; *) - exe=_build/default/topbin/coqtop_byte_bin.bc + exe=_build/default/topbin/coqc_bin.bc ;; esac -ocamldebug $(ocamlfind query -recursive -i-format coq.top_printers) -I +threads -I dev $exe +emacs="${INSIDE_EMACS:+-emacs}" + +ocamldebug $emacs $(ocamlfind query -recursive -i-format coq.top_printers) -I +threads -I dev $exe "$@" |