diff options
Diffstat (limited to 'dev/db')
| -rw-r--r-- | dev/db | 4 |
1 files changed, 0 insertions, 4 deletions
@@ -28,12 +28,8 @@ install_printer Top_printers.pptype install_printer Top_printers.ppj 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.ppevm -install_printer Top_printers.ppclenv install_printer Top_printers.pptac install_printer Top_printers.ppobj |