diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2004-04-24 11:07:12 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2004-04-24 11:07:12 +0000 |
| commit | 9534a90440aa813824eba17ed17d9d62832d35dc (patch) | |
| tree | 67b9e9ad0a78215cd375c35e4de3a86c4c9b4f5a /doc/PG-adapting.texi | |
| parent | dab8ee05775e82974bed947d585037e1c1d9e64b (diff) | |
Spacing
Diffstat (limited to 'doc/PG-adapting.texi')
| -rw-r--r-- | doc/PG-adapting.texi | 7 |
1 files changed, 1 insertions, 6 deletions
diff --git a/doc/PG-adapting.texi b/doc/PG-adapting.texi index f4fbe1cc..86cc1601 100644 --- a/doc/PG-adapting.texi +++ b/doc/PG-adapting.texi @@ -1933,8 +1933,6 @@ scripting (to do undo operations), the whole history is discarded. @end defvar @c TEXI DOCSTRING MAGIC: proof-shell-require-command-regexp - - @defvar proof-shell-require-command-regexp A regular expression to match a Require-type of command, or nil.@* If set to a regexp, then @samp{@code{proof-done-advancing-require-function}} @@ -1944,11 +1942,8 @@ This can be used to adjust @samp{@code{proof-included-files-list}} based on the lines of script that have been processed/parsed, rather than relying on information from the prover. @end defvar -@c TEXI DOCSTRING MAGIC: proof-done-advancing-require-function - - - +@c TEXI DOCSTRING MAGIC: proof-done-advancing-require-function @defvar proof-done-advancing-require-function Invoked from @samp{@code{proof-done-advancing}}, see @samp{@code{proof-shell-require-command-regexp}}.@* The function is passed the span and the command as arguments. |