diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-05-26 15:04:21 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-05-26 15:04:21 +0200 |
| commit | ec5ef15aae0d6f900eb4a8e6ba61c0952c993eb3 (patch) | |
| tree | effab6623d87f23bcbb65a1fe093f8a8fd4dd429 /library/global.mli | |
| parent | c4ffe2b6725a3f8f60763228b77668aa3444f79c (diff) | |
Jump to error line in CoqIDE grabs focus of the textview.
Diffstat (limited to 'library/global.mli')
0 files changed, 0 insertions, 0 deletions