diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/sphinx/practical-tools/coqide.rst | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/doc/sphinx/practical-tools/coqide.rst b/doc/sphinx/practical-tools/coqide.rst index ab7fe2ac08..44955412ce 100644 --- a/doc/sphinx/practical-tools/coqide.rst +++ b/doc/sphinx/practical-tools/coqide.rst @@ -307,6 +307,11 @@ Each of the file tokens provided may consists of one of: - the token ``local``, which resolves to the `coqide.bindings` file stored in the user configuration directory. +Remark: if a filename other than the first one includes a "~" to refer +to the home directory, it won't be expanded properly. To work around that +issue, one should not use comas but instead repeat the flag, in the form: +``-unicode-bindings file1 .. -unicode-bindings fileN``. + Remark: if two bindings for a same token both have the same priority value (or both have no priority value set), then the binding considered is the one from the file that comes first on the command line. |