From d9552de21522f19f7656a6b635dee1e325262e09 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 4 Jan 2006 16:33:53 +0000
Subject: 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
---
 dev/db | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'dev/db')

diff --git a/dev/db b/dev/db
index 9ee08bc406..54e0706cc6 100644
--- a/dev/db
+++ b/dev/db
@@ -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
+                                                  
 
-- 
cgit v1.2.3