From a47a249e8c31dece9b816bc49d6c5a2aa50fb21b Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 12 Sep 2017 20:06:35 +0200
Subject: Reference manual: A few words about the file system constraints for
 -Q/-R.

---
 doc/refman/RefMan-com.tex | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex
index 45230fb6e5..036fc9368d 100644
--- a/doc/refman/RefMan-com.tex
+++ b/doc/refman/RefMan-com.tex
@@ -106,6 +106,15 @@ The following command-line options are recognized by the commands {\tt
   recursively available from {\Coq} using absolute names (extending
   the {\dirpath} prefix) (see Section~\ref{LongNames}).
 
+  Note that only those subdirectories and files which obey the lexical
+  conventions of what is an {\ident} (see Section~\ref{lexical})
+  are taken into account. Conversely, the underlying file systems or
+  operating systems may be more restrictive than {\Coq}. While Linux's
+  ext4 file system supports any {\Coq} recursive layout
+  (within the limit of 255 bytes per file name), the default on NTFS
+  (Windows) or HFS+ (MacOS X) file systems is on the contrary to
+  disallow two files differing only in the case in the same directory.
+
   \SeeAlso Section~\ref{Libraries}.
 
 \item[{\tt -R} {\em directory} {\dirpath}]\ %
-- 
cgit v1.2.3