From 039ff3a61a3d38148df8a899ad4c4c11673f05a8 Mon Sep 17 00:00:00 2001
From: Patrick Loiseleur
Date: Mon, 17 May 1999 13:43:12 +0000
Subject: 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
---
 doc/ProofGeneral.texi | 9 +++++++++
 1 file changed, 9 insertions(+)

(limited to 'doc')

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 
-- 
cgit v1.2.3