From b213bae73ca927874275a896482246b2ee761b7b Mon Sep 17 00:00:00 2001
From: gareuselesinge
Date: Thu, 8 Aug 2013 18:52:17 +0000
Subject: Support Proof General

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16678 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 interp/constrintern.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'interp')

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 6013a3abfd..4ab85e0e6c 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -686,7 +686,7 @@ let check_no_explicitation l =
 
 (* This code is taken from dumpglob, and should be shared with it *)
 let feedback_global loc ref =
-  if !Flags.ide_slave then
+  if !Flags.ide_slave || !Flags.print_emacs then
     let remove_sections dir =
       if Libnames.is_dirpath_prefix_of dir (Lib.cwd ()) then
         Libnames.pop_dirpath_n (Lib.sections_depth ()) (Lib.cwd ())
-- 
cgit v1.2.3