aboutsummaryrefslogtreecommitdiff
path: root/dev/dune-dbg.in
diff options
context:
space:
mode:
authorGaëtan Gilbert2021-03-23 11:28:07 +0100
committerGaëtan Gilbert2021-03-23 11:28:07 +0100
commit3bdfd3a8b4f2e00c0529c0d194f75c4c78dd8ee0 (patch)
tree57ac3ea212be0fbafd6488f0a305054f9663cf7b /dev/dune-dbg.in
parent1f7875b9c457aad27cd5ee8bfe2dd12898926cb2 (diff)
Fix debug printers
Diffstat (limited to 'dev/dune-dbg.in')
-rwxr-xr-xdev/dune-dbg.in2
1 files changed, 1 insertions, 1 deletions
diff --git a/dev/dune-dbg.in b/dev/dune-dbg.in
index 47dfbad3a0..cc8574c6d6 100755
--- a/dev/dune-dbg.in
+++ b/dev/dune-dbg.in
@@ -26,4 +26,4 @@ esac
emacs="${INSIDE_EMACS:+-emacs}"
-ocamldebug $emacs $(ocamlfind query -recursive -i-format coq.top_printers) -I +threads -I dev $exe "$@"
+ocamldebug $emacs $(ocamlfind query -recursive -i-format coq-core.top_printers) -I +threads -I dev $exe "$@"