diff options
author | 2017-04-27 12:05:51 -0400 | |
---|---|---|
committer | 2017-04-27 12:05:51 -0400 | |
commit | e574b4bdd974daa7d2ceecf799762be92fadff44 (patch) | |
tree | a4fd54fedd13150bd30cedd1778634bb2344af9b /doc | |
parent | 746066172b8ed508886feb20cee239920ca7a4c7 (diff) |
fix order of command-line arguments mentioned in Add LoadPath
Diffstat (limited to 'doc')
-rw-r--r-- | doc/refman/RefMan-oth.tex | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex index 56ce753cd..a25da7d92 100644 --- a/doc/refman/RefMan-oth.tex +++ b/doc/refman/RefMan-oth.tex @@ -697,8 +697,8 @@ which can be any valid path. \subsection[\tt Add LoadPath {\str} as {\dirpath}.]{\tt Add LoadPath {\str} as {\dirpath}.\comindex{Add LoadPath}\label{AddLoadPath}} -This command is equivalent to the command line option {\tt -Q {\dirpath} - {\str}}. It adds the physical directory {\str} to the current {\Coq} +This command is equivalent to the command line option {\tt -Q {\str} + {\dirpath}}. It adds the physical directory {\str} to the current {\Coq} loadpath and maps it to the logical directory {\dirpath}. \begin{Variants} @@ -707,8 +707,8 @@ Performs as {\tt Add LoadPath {\str} as {\dirpath}} but for the empty directory \end{Variants} \subsection[\tt Add Rec LoadPath {\str} as {\dirpath}.]{\tt Add Rec LoadPath {\str} as {\dirpath}.\comindex{Add Rec LoadPath}\label{AddRecLoadPath}} -This command is equivalent to the command line option {\tt -R {\dirpath} - {\str}}. It adds the physical directory {\str} and all its +This command is equivalent to the command line option {\tt -R {\str} + {\dirpath}}. It adds the physical directory {\str} and all its subdirectories to the current {\Coq} loadpath. \begin{Variants} |