diff options
| author | Hugo Herbelin | 2019-04-27 12:38:05 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2019-04-30 12:56:13 +0200 |
| commit | bae9b53c58d995a0cce404c279c37206e5418d2f (patch) | |
| tree | 0218021d58b771380614121f4a6816fa271840b8 /dev | |
| parent | d42c059d6c7877948fdae76bf0400d4e3b06b90d (diff) | |
CoqIDE nanoPG: adding keys to go the start/end of file (w/o evaluating).
On MacOS X: Ctrl-Cmd-Left and Ctrl-Cmd-Right
Elsewhere: Meta-Left and Meta-Right
See issue #9899 (moving cursor to beginning and end of file).
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions