diff options
Diffstat (limited to 'dev/dune-dbg.in')
| -rwxr-xr-x | dev/dune-dbg.in | 12 |
1 files changed, 11 insertions, 1 deletions
diff --git a/dev/dune-dbg.in b/dev/dune-dbg.in index 1382f4d1b6..498f167eb1 100755 --- a/dev/dune-dbg.in +++ b/dev/dune-dbg.in @@ -7,11 +7,21 @@ case $1 in exe=_build/default/checker/coqchk.bc ;; coqide) + shift exe=_build/default/ide/coqide_main.bc ;; - *) + coqc) + shift exe=_build/default/topbin/coqc_bin.bc ;; + coqtop) + shift + exe=_build/default/topbin/coqtop_byte_bin.bc + ;; + *) + echo "First argument must be one of {coqc,coqtop,checker,coqide}" + exit 1 + ;; esac emacs="${INSIDE_EMACS:+-emacs}" |