diff options
| author | Emilio Jesus Gallego Arias | 2020-06-11 16:38:48 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-06-11 16:38:48 +0200 |
| commit | 7fb7c9ede2b44bac35b08d810ec9a08358d0267b (patch) | |
| tree | 8f0e599544f33c7207b5a8f954d51a02e9c1415b /dev/dune-dbg.in | |
| parent | 149d9604c56969a067ee6d9d0d51919d96cbdc7f (diff) | |
[dune] [dbg] Fix coqide target after CoqIDE move.
Fixes #12496
Diffstat (limited to 'dev/dune-dbg.in')
| -rwxr-xr-x | dev/dune-dbg.in | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/dev/dune-dbg.in b/dev/dune-dbg.in index 498f167eb1..47dfbad3a0 100755 --- a/dev/dune-dbg.in +++ b/dev/dune-dbg.in @@ -8,7 +8,7 @@ case $1 in ;; coqide) shift - exe=_build/default/ide/coqide_main.bc + exe=_build/default/ide/coqide/coqide_main.bc ;; coqc) shift |