diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-09-12 20:06:35 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-09-13 19:00:42 +0200 |
| commit | a47a249e8c31dece9b816bc49d6c5a2aa50fb21b (patch) | |
| tree | 946b9d2cbe24ddb6f56975ec58e0c0fcd68d734d /doc | |
| parent | 98e2b048aa5419ac3d075e1d3f2499cb816fe92e (diff) | |
Reference manual: A few words about the file system constraints for -Q/-R.
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/refman/RefMan-com.tex | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex index 45230fb6e..036fc9368 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}]\ % |