From f0e04793cdecaf3dd9c57b10b3b2fc12898cf6e7 Mon Sep 17 00:00:00 2001
From: gareuselesinge
Date: Tue, 1 Oct 2013 15:35:32 +0000
Subject: CoqIDE: do not print cmd_stack too often

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16831 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 ide/coqOps.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index 0dea01cd52..b30f7cbd98 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -309,8 +309,7 @@ object(self)
     let stop = start_sentence#forward_chars post in
     let markup = lazy text in
     buffer#apply_tag Tags.Script.tooltip ~start ~stop;
-    add_tooltip sentence pre post markup;
-    self#print_stack
+    add_tooltip sentence pre post markup
 
   method private is_dummy_id id =
     match id with
-- 
cgit v1.2.3