diff options
Diffstat (limited to 'dev/db')
| -rw-r--r-- | dev/db | 3 |
1 files changed, 1 insertions, 2 deletions
@@ -1,5 +1,3 @@ -load_printer "gramlib.cma" -load_printer "str.cma" load_printer "printers.cma" install_printer Top_printers.ppfuture @@ -13,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 |