diff options
| author | Hugo Herbelin | 2019-04-27 22:19:15 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2019-04-27 22:19:15 +0200 |
| commit | 9b2cbdcdaac203999484ef90225f6cba5e8052db (patch) | |
| tree | 6fc2fb3cbbd8d3eb853fcf87c0218cca32bc6f37 /doc/plugin_tutorial/tuto1 | |
| parent | ae4239d6a5f4afcd9b7321dba790ffd4a64994a1 (diff) | |
CoqiDE: Load coqide.keys after coqiderc (addressing part of #9899).
This avoids the modifiers keys to overwrite changes made in
coqide.keys.
Diffstat (limited to 'doc/plugin_tutorial/tuto1')
0 files changed, 0 insertions, 0 deletions