diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-01-04 16:33:53 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-01-04 16:33:53 +0000 |
| commit | d9552de21522f19f7656a6b635dee1e325262e09 (patch) | |
| tree | 5ef2b74415a94d78371d24da9813b9a8fd753512 /dev/db | |
| parent | 6552e154318f590336ae2226ba615b9e4cca0608 (diff) | |
Affichage concis des locations (si jamais ppterm/pprawterm sont débranchés)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7786 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'dev/db')
| -rw-r--r-- | dev/db | 4 |
1 files changed, 3 insertions, 1 deletions
@@ -29,5 +29,7 @@ install_printer Top_printers.prevd install_printer Top_printers.prclenv install_printer Top_printers.pptac -install_printer Top_printers.pr_obj +install_printer Top_printers.pr_obj +install_printer Top_printers.pploc + |