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_MessageView.ml | 1 + 1 file changed, 1 insertion(+) (limited to 'ide/wg_MessageView.ml') diff --git a/ide/wg_MessageView.ml b/ide/wg_MessageView.ml index 09f1d4453..b32674084 100644 --- a/ide/wg_MessageView.ml +++ b/ide/wg_MessageView.ml @@ -48,6 +48,7 @@ let message_view () : message_view = ~source_buffer:buffer ~packing:scroll#add ~editable:false ~cursor_visible:false ~wrap_mode:`WORD () in + let () = Gtk_parsing.fix_double_click view in let default_clipboard = GData.clipboard Gdk.Atom.primary in let _ = buffer#add_selection_clipboard default_clipboard in let () = view#set_left_margin 2 in -- cgit v1.2.3