From 8d93141a931a4007feb8f28df2cd61c7b1c1b61e Mon Sep 17 00:00:00 2001
From: charguer
Date: Wed, 14 Nov 2018 12:53:38 +0100
Subject: final polishing for coqide bindings

---
 doc/sphinx/practical-tools/coqide.rst | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'doc/sphinx')

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.
-- 
cgit v1.2.3