1 files changed, 1 insertions, 0 deletions
diff --git a/dev/db b/dev/db
index 2cb7bb5f3d..77a995aa3f 100644
--- a/dev/db
+++ b/dev/db
@@ -1,3 +1,4 @@
+load_printer "gramlib.cma"
 load_printer "top_printers.cmo"
 install_printer Top_printers.prid
 install_printer Top_printers.prsp