diff options
| author | Pierre Courtieu | 2015-03-26 16:40:23 +0000 |
|---|---|---|
| committer | Pierre Courtieu | 2015-03-26 16:40:23 +0000 |
| commit | a8e3c5e6d52bbf52bee76dd1609b7fca9bd48f3e (patch) | |
| tree | af0a3e459ffde6f3e2bc5a8d8315ecbb63bf3728 | |
| parent | f9663fdac4e0204b535abb9a6ff509e5717a82a0 (diff) | |
A remark about project file in the documentation.
Saying that one -arg should be followed by only one option. For
several options, put several -arg, ONE PER LINE.
| -rw-r--r-- | coq/coq.el | 3 | ||||
| -rw-r--r-- | doc/ProofGeneral.texi | 4 |
2 files changed, 6 insertions, 1 deletions
@@ -1221,7 +1221,8 @@ alreadyopen is t if buffer already existed." ;; match-string 1 must contain the string to add to coqtop command line, so we ;; ignore -arg, we use numbered subregexpr. (defconst coq-prog-args-regexp - "\\_<\\(?1:-opt\\|-byte\\)\\|-arg\\(?:[[:space:]]+\\(?1:[^ \t\n#]+\\)\\)?") + "\\_<\\(?1:-opt\\|-byte\\)\\|-arg\\(?:[[:space:]]+\\(?1:[^\t\n#]+\\)\\)?") + (defun coq-read-option-from-project-file (projectbuffer regexp &optional dirprefix) "look for occurrences of regexp in buffer projectbuffer and collect subexps. diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi index 25642efb..20b7bed6 100644 --- a/doc/ProofGeneral.texi +++ b/doc/ProofGeneral.texi @@ -4325,6 +4325,10 @@ parsed by ProofGeneral to guess the command line option. In this example the command line built by Proofgeneral will be @code{coqtop -foo3 -R foo bar -I foo2}. +@emph{Remarque:} @code{-arg} must be followed by one and only one option +to pass to coqtop/coqc, use several @code{-arg} to issue several +options. One per line (limitation of proofgeneral). + This is the recommended way of configuring coqtop options for coq compilation, CoqIde and Proofgeneral. Its main advantage is that it avoids duplicating informations between these three tools. |