aboutsummaryrefslogtreecommitdiff
path: root/dev/dune_db_408
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/dune_db_408
parentdaca83946ed5a001f2461fefa787a80f7dcdea01 (diff)
parent129e935dd950191d01f9bfba17889ae1ca49d34b (diff)
Merge PR #12958: Fix load_printers after zarith
Reviewed-by: ejgallego
Diffstat (limited to 'dev/dune_db_408')
-rw-r--r--dev/dune_db_4081
1 files changed, 1 insertions, 0 deletions
diff --git a/dev/dune_db_408 b/dev/dune_db_408
index 3bf13da62d..5f826fe383 100644
--- a/dev/dune_db_408
+++ b/dev/dune_db_408
@@ -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