aboutsummaryrefslogtreecommitdiff
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
parent1f7875b9c457aad27cd5ee8bfe2dd12898926cb2 (diff)
Fix debug printers
-rwxr-xr-xdev/dune-dbg.in2
-rw-r--r--dev/top_printers.dbg1
2 files changed, 1 insertions, 2 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 "$@"
diff --git a/dev/top_printers.dbg b/dev/top_printers.dbg
index fe95a59d9b..5d37c60bca 100644
--- a/dev/top_printers.dbg
+++ b/dev/top_printers.dbg
@@ -12,7 +12,6 @@ install_printer Top_printers.ppmind
install_printer Top_printers.ppind
install_printer Top_printers.ppsp
install_printer Top_printers.ppqualid
-install_printer Top_printers.ppclindex
install_printer Top_printers.ppscheme
install_printer Top_printers.ppwf_paths
install_printer Top_printers.ppevar