1 files changed, 2 insertions, 1 deletions

diff --git a/dev/db b/dev/db
index 86e35a3ec..1282352e6 100644
--- a/dev/db
+++ b/dev/db
@@ -1,4 +1,5 @@
-load_printer "printers.cma"
+source core.dbg
+load_printer top_printers.cmo
 
 install_printer Top_printers.ppfuture