diff options
Diffstat (limited to 'dev/db')
| -rw-r--r-- | dev/db | 35 |
1 files changed, 35 insertions, 0 deletions
@@ -0,0 +1,35 @@ +load_printer "gramlib.cma" +load_printer "top_printers.cmo" +install_printer Top_printers.prid +install_printer Top_printers.prlab +install_printer Top_printers.prmsid +install_printer Top_printers.prmbid +install_printer Top_printers.prdir +install_printer Top_printers.prmp +install_printer Top_printers.prkn +install_printer Top_printers.prsp +install_printer Top_printers.prqualid +install_printer Top_printers.prast +install_printer Top_printers.prastpat +install_printer Top_printers.prastpatl + +install_printer Top_printers.pppattern +install_printer Top_printers.pprawterm + +install_printer Top_printers.ppterm +install_printer Top_printers.print_uni +install_printer Top_printers.pp_universes +install_printer Top_printers.pptype +install_printer Top_printers.prj + +install_printer Top_printers.prgoal +install_printer Top_printers.prsigmagoal +install_printer Top_printers.pproof +install_printer Top_printers.prevd +install_printer Top_printers.prevc +install_printer Top_printers.prwc +install_printer Top_printers.prclenv + +install_printer Top_printers.pptac +install_printer Top_printers.pr_obj + |