aboutsummaryrefslogtreecommitdiff
path: root/dev/core.dbg
diff options
context:
space:
mode:
authorcoqbot-app[bot]2020-08-31 17:36:34 +0000
committerGitHub2020-08-31 17:36:34 +0000
commit84a32bbdf6572a45a78667803e574a561bbed21f (patch)
treea91cd50fd7c6e41719580d54e346b6b8a6c9d790 /dev/core.dbg
parentdaca83946ed5a001f2461fefa787a80f7dcdea01 (diff)
parent129e935dd950191d01f9bfba17889ae1ca49d34b (diff)
Merge PR #12958: Fix load_printers after zarith
Reviewed-by: ejgallego
Diffstat (limited to 'dev/core.dbg')
-rw-r--r--dev/core.dbg1
1 files changed, 1 insertions, 0 deletions
diff --git a/dev/core.dbg b/dev/core.dbg
index ec946e2df0..6d52bae773 100644
--- a/dev/core.dbg
+++ b/dev/core.dbg
@@ -1,5 +1,6 @@
load_printer threads.cma
load_printer str.cma
+load_printer zarith.cma
load_printer config.cma
load_printer clib.cma
load_printer dynlink.cma