aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev/base_db
blob: b540aed6ca9f37cea6c60613ae7618c59ef9e58a (plain)
1
2
3
4
5
6
load_printer "gramlib.cma"
load_printer "top_printers.cmo"
install_printer Top_printers.prid
install_printer Top_printers.prsp
install_printer Top_printers.print_pure_constr