summaryrefslogtreecommitdiff
path: root/dev/db
diff options
context:
space:
mode:
Diffstat (limited to 'dev/db')
-rw-r--r--dev/db2
1 files changed, 2 insertions, 0 deletions
diff --git a/dev/db b/dev/db
index 36a171af..f226291d 100644
--- a/dev/db
+++ b/dev/db
@@ -11,6 +11,7 @@ install_printer Top_printers.ppexistentialset
install_printer Top_printers.ppintset
install_printer Top_printers.pplab
install_printer Top_printers.ppdir
+install_printer Top_printers.ppmbid
install_printer Top_printers.ppmp
install_printer Top_printers.ppkn
install_printer Top_printers.ppcon
@@ -50,6 +51,7 @@ install_printer Top_printers.prsubst
install_printer Top_printers.prdelta
install_printer Top_printers.ppfconstr
install_printer Top_printers.ppgenarginfo
+install_printer Top_printers.ppgenargargt
install_printer Top_printers.ppist
install_printer Top_printers.ppconstrunderbindersidmap
install_printer Top_printers.ppunbound_ltac_var_map