From 49d8a6c11c2f0e6a7abb942980ebad3bcbb3456a Mon Sep 17 00:00:00 2001
From: gareuselesinge
Date: Mon, 19 Aug 2013 12:27:10 +0000
Subject: Tooltips can be augmented with custom widgets, still not clickable

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

diff --git a/ide/wg_Tooltip.ml b/ide/wg_Tooltip.ml
index c3ed8c32e0..62598dd509 100644
--- a/ide/wg_Tooltip.ml
+++ b/ide/wg_Tooltip.ml
@@ -36,6 +36,7 @@ let tooltip_callback (view : GText.view) ~x ~y ~kbd tooltip =
     try
       let ss = Table.find_all table iter#offset in
       let msg = String.concat "\n" (CList.uniquize (List.map Lazy.force ss)) in
+      GtkBase.Tooltip.set_icon_from_stock tooltip `INFO `BUTTON;
       view#misc#set_tooltip_markup ("<tt>" ^ msg ^ "</tt>")
     with Not_found -> ()
   end else begin
-- 
cgit v1.2.3