From 2a642fd654e91a4dd491917a12f0c19e617de159 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Thu, 2 May 2024 16:30:12 +0200 Subject: [PATCH] load_printer memprof_limits.cma in dev/db When memprof-limits is installed, lib depends on it and all loads after it fail if we don't load memprof-limits explicitly. When it is not installed, loading memprof_limits fails but the other loads still work. Therefore I think trying to load it is better. --- dev/db | 1 + 1 file changed, 1 insertion(+) diff --git a/dev/db b/dev/db index 4234b37ab9fc..0d7a66ea3b7c 100644 --- a/dev/db +++ b/dev/db @@ -5,6 +5,7 @@ load_printer config.cma load_printer boot.cma load_printer clib.cma load_printer coqperf.cma +load_printer memprof_limits.cma load_printer lib.cma load_printer gramlib.cma load_printer coqrun.cma