diff options
| author | Hugo Herbelin | 2019-06-16 13:58:41 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2019-09-10 15:20:58 +0200 |
| commit | bc10e4566cefcab6449fb97b47cf23a431c5e8bb (patch) | |
| tree | 48fa72ebffc60500d37775d3331c6c3472155851 /doc | |
| parent | 36bc8d2b666457c18436c1801d7ba811ed2c2067 (diff) | |
Refman: To be compatible gtk2/gtk3, not mentioning GTK+ version explicitely.
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/sphinx/practical-tools/coqide.rst | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/sphinx/practical-tools/coqide.rst b/doc/sphinx/practical-tools/coqide.rst index 92b7fd403c..b1f392c337 100644 --- a/doc/sphinx/practical-tools/coqide.rst +++ b/doc/sphinx/practical-tools/coqide.rst @@ -184,7 +184,7 @@ Notice that these settings are saved in the file ``coqiderc`` in the is the value of ``$XDG_CONFIG_HOME`` if this environment variable is set and which otherwise is ``$HOME/.config/``. -A Gtk2 accelerator keymap is saved under the name ``coqide.keys`` in +A GTK+ accelerator keymap is saved under the name ``coqide.keys`` in the same ``coq`` subdirectory of the user configuration directory. It is not recommended to edit this file manually: to modify a given menu shortcut, go to the corresponding menu item without releasing the |