diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2000-03-23 16:37:19 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2000-03-23 16:37:19 +0000 |
| commit | 0a7ae8a38680d573605eaa27139c5b430c6daf30 (patch) | |
| tree | e36df67e5857707e3c3c0b5368660101edec64ce /doc | |
| parent | c64deab10f68f15b62ce36adf2970825c7b091de (diff) | |
Made magic.
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/ProofGeneral.texi | 13 |
1 files changed, 8 insertions, 5 deletions
diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi index b3c22fa6..5f00f69e 100644 --- a/doc/ProofGeneral.texi +++ b/doc/ProofGeneral.texi @@ -448,6 +448,7 @@ tested pre-releases or sent bug reports, including Pascal Brisset, Martin Buechi, Matt Fairtlough, +Kim Hyung Ho, John Longley, Tobias Nipkow, Leonor Prensa-Nieto, @@ -4148,13 +4149,15 @@ A list of escapes that are applied to %s for filenames.@* A list of cons cells, car of which is string to be replaced by the cdr. For example, when directories are sent to Isabelle, HOL, and Coq, -they appear inside ML strings and the backslash character must -be escaped. The setting +they appear inside ML strings and the backslash character and +quote characters must be escaped. The setting @lisp - '(("\\" . "\\")) + '(("@var{\\\\}" . "@var{\\\\}") + ("\"" . "\\\"")) @end lisp -achieves this. This does not apply to @var{lego}, which does not -need escapes. +achieves this. This does not apply to @var{lego}, which does not +need backslash escapes and does not allow filenames with +quote characters. @end defvar @c TEXI DOCSTRING MAGIC: proof-shell-process-connection-type |