From 1d39965a694698c3df238fc424203c6b77b067e7 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 15 Feb 2015 20:30:15 +0100
Subject: Selecting whole words on double-click in CoqIDE.

Fixes bug #4026.
---
 ide/wg_ScriptView.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'ide/wg_ScriptView.ml')

diff --git a/ide/wg_ScriptView.ml b/ide/wg_ScriptView.ml
index 5d21efd956..8298d9954f 100644
--- a/ide/wg_ScriptView.ml
+++ b/ide/wg_ScriptView.ml
@@ -418,6 +418,7 @@ object (self)
       self#buffer#end_user_action ()
 
   initializer
+    let () = Gtk_parsing.fix_double_click self in
     let supersed cb _ =
       let _ = cb () in
       GtkSignal.stop_emit()
-- 
cgit v1.2.3