diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-02-15 20:30:15 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-02-15 20:39:09 +0100 |
| commit | 1d39965a694698c3df238fc424203c6b77b067e7 (patch) | |
| tree | fda16c48cca35c65aa5f852f7c9d69bbfeedc965 /ide/wg_ScriptView.ml | |
| parent | 7d3ab7e00453e259939535618e4e10c624a37ec9 (diff) | |
Selecting whole words on double-click in CoqIDE.
Fixes bug #4026.
Diffstat (limited to 'ide/wg_ScriptView.ml')
| -rw-r--r-- | ide/wg_ScriptView.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/ide/wg_ScriptView.ml b/ide/wg_ScriptView.ml index 5d21efd95..8298d9954 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() |