From 6b2d6dc14fdc3f8c0b71843c88c3903d0394f5e2 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Thu, 28 Jul 2011 17:20:11 +0000
Subject: Ide_slave: same attributes for { } and Focus/Unfocus (fix coqide
 display)

 Without this, coqide display a copy of the goal in its
 response buffer...

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14310 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 toplevel/ide_slave.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml
index 41f200b4fe..4d1574e8c3 100644
--- a/toplevel/ide_slave.ml
+++ b/toplevel/ide_slave.ml
@@ -166,8 +166,8 @@ let rec attribute_of_vernac_command = function
   | VernacProof _ -> []
 
   | VernacProofMode _ -> []
-  | VernacSubproof _ -> []
-  | VernacEndSubproof -> []
+  | VernacSubproof _ -> [SolveCommand]
+  | VernacEndSubproof -> [SolveCommand]
 
   (* Toplevel control *)
   | VernacToplevelControl _ -> []
-- 
cgit v1.2.3