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/ideutils.ml | |
parent | 7d3ab7e00453e259939535618e4e10c624a37ec9 (diff) |
Selecting whole words on double-click in CoqIDE.
Fixes bug #4026.
Diffstat (limited to 'ide/ideutils.ml')
0 files changed, 0 insertions, 0 deletions