diff options
| author | Patrick Loiseleur | 1999-05-17 13:43:12 +0000 |
|---|---|---|
| committer | Patrick Loiseleur | 1999-05-17 13:43:12 +0000 |
| commit | 039ff3a61a3d38148df8a899ad4c4c11673f05a8 (patch) | |
| tree | a7fb04bfaef6a738976d257f57fcf000e8245aa9 /doc | |
| parent | 3a500cef5174cf878cc38f002d46a400547445b4 (diff) | |
I've added the custom option 'prog-name-guess' in the generic part and
the function coq-guess-command-line in the coq part. Every prover
should have the functon *-guess-command-line that uses, for example,
the output of "make -n" to guess the correct command line options of
the prover.
Patrick
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/ProofGeneral.texi | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi index 15bab2f4..76640043 100644 --- a/doc/ProofGeneral.texi +++ b/doc/ProofGeneral.texi @@ -1587,6 +1587,15 @@ If non-nil, query user which program to run for the inferior process. The default value is @code{nil}. @end defopt +@c TEXI DOCSTRING MAGIC: proof-prog-name-guess +@defopt proof-prog-name-guess +If non-nil, ProofGeneral tries to run `make -n' to guess +the command line arguments for the proof assistant +(Currently implemented for Coq only) + +The default value is @code{nil}. +@end defopt + @c TEXI DOCSTRING MAGIC: proof-rsh-command @defopt proof-rsh-command |