diff options
| -rw-r--r-- | ide/coqOps.ml | 3 |
1 files changed, 1 insertions, 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 |