aboutsummaryrefslogtreecommitdiff
path: root/dev/core.dbg
diff options
context:
space:
mode:
authorGaëtan Gilbert2018-10-26 13:28:15 +0200
committerGaëtan Gilbert2018-10-26 13:28:15 +0200
commit3b14b406807af5503471d4936dea4d5ed0e0c789 (patch)
treecdbda0f6706c0b2be87cf32fb87b7e5551fffd25 /dev/core.dbg
parenta5854e84d083a6caf045d424ec34d47a9ffebcc4 (diff)
parent1db19a8f454e0f8c5a60101c87ccd38e0883d530 (diff)
Merge PR #8753: [build] Refactoring of config lib and ocamldebug tweaks.
Diffstat (limited to 'dev/core.dbg')
-rw-r--r--dev/core.dbg4
1 files changed, 2 insertions, 2 deletions
diff --git a/dev/core.dbg b/dev/core.dbg
index 972ba701e4..f676b643e4 100644
--- a/dev/core.dbg
+++ b/dev/core.dbg
@@ -1,6 +1,7 @@
-source camlp5.dbg
load_printer threads.cma
load_printer str.cma
+load_printer gramlib.cma
+load_printer config.cma
load_printer clib.cma
load_printer dynlink.cma
load_printer lib.cma
@@ -16,4 +17,3 @@ load_printer tactics.cma
load_printer vernac.cma
load_printer stm.cma
load_printer toplevel.cma
-load_printer ltac_plugin.cmo