From 153b68664adb03dde1325bdb77fa371d5aa8ff7e Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 19 Nov 2018 15:47:12 +0100
Subject: CoqIDE: No more explicit activation of tooltips on toolbar.

According to
https://developer.gnome.org/gtk2/stable/GtkToolbar.html#gtk-toolbar-set-tooltips,
tooltips are now managed globally by gtk-enable-tooltips which is true by default.
---
 ide/coqide.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/ide/coqide.ml b/ide/coqide.ml
index 386bd8047c..e977ec5320 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -1220,7 +1220,7 @@ let build_ui () =
       ((Coqide_ui.ui_m#get_widget "/CoqIde ToolBar")#as_widget)
   in
   let () = GtkButton.Toolbar.set
-    ~orientation:`HORIZONTAL ~style:`ICONS ~tooltips:true tbar
+    ~orientation:`HORIZONTAL ~style:`ICONS tbar
   in
   let toolbar = new GButton.toolbar tbar in
   let () = vbox#pack toolbar#coerce in
-- 
cgit v1.2.3