diff options
Diffstat (limited to 'dev/db')
| -rw-r--r-- | dev/db | 4 |
1 files changed, 4 insertions, 0 deletions
@@ -3,6 +3,7 @@ load_printer "printers.cma" install_printer Top_printers.ppid install_printer Top_printers.ppidset +install_printer Top_printers.ppintset install_printer Top_printers.pplab install_printer Top_printers.ppmsid install_printer Top_printers.ppmbid @@ -20,6 +21,7 @@ install_printer Top_printers.pprawconstr install_printer Top_printers.ppconstr install_printer Top_printers.ppuni install_printer Top_printers.ppuniverses +install_printer Top_printers.ppconstraints install_printer Top_printers.pptype install_printer Top_printers.ppj install_printer Top_printers.ppenv @@ -27,6 +29,7 @@ install_printer Top_printers.ppenv install_printer Top_printers.ppgoal install_printer Top_printers.ppsigmagoal install_printer Top_printers.pproof +install_printer Top_printers.ppmetas install_printer Top_printers.ppevd install_printer Top_printers.ppevm install_printer Top_printers.ppclenv @@ -34,5 +37,6 @@ install_printer Top_printers.ppclenv install_printer Top_printers.pptac install_printer Top_printers.ppobj install_printer Top_printers.pploc +install_printer Top_printers.prsubst |