diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-10-05 18:49:12 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-10-05 18:49:12 +0200 |
| commit | 73620255a7a62703a89026336f97a4bc8a913afd (patch) | |
| tree | 0b28d62d27b3fe6e94a07845ca8900cc9b3c9a71 /doc | |
| parent | f78a39499ef210456dd96ecb9896874c9ce300ae (diff) | |
| parent | a47a249e8c31dece9b816bc49d6c5a2aa50fb21b (diff) | |
Merge PR #1041: Miscellaneous fixes about UTF-8 (including a fix to BZ#5715 to escape non-UTF-8 file names)
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 9790111f1..892c9931b 100644 --- a/doc/refman/RefMan-com.tex +++ b/doc/refman/RefMan-com.tex @@ -107,6 +107,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}]\ % |