From a8e3c5e6d52bbf52bee76dd1609b7fca9bd48f3e Mon Sep 17 00:00:00 2001 From: Pierre Courtieu Date: Thu, 26 Mar 2015 16:40:23 +0000 Subject: 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. --- doc/ProofGeneral.texi | 4 ++++ 1 file changed, 4 insertions(+) (limited to 'doc') 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. -- cgit v1.2.3