diff options
author | Hendrik Tews <hendrik@askra.de> | 2011-05-05 09:18:23 +0000 |
---|---|---|
committer | Hendrik Tews <hendrik@askra.de> | 2011-05-05 09:18:23 +0000 |
commit | 2cd8b2cd5cb166c46a1b76cd527d1b98d778ec9e (patch) | |
tree | 544366ce160cb7cc7b93e358fee04c2255a36049 /doc/PG-adapting.texi | |
parent | 74bbc32ad24ee7fea5ecabfeea951b96de27baa4 (diff) |
- flushed proof-done-advancing-require-function and
proof-shell-require-command-regexp
- TAGS updated to really flush them
Diffstat (limited to 'doc/PG-adapting.texi')
-rw-r--r-- | doc/PG-adapting.texi | 15 |
1 files changed, 1 insertions, 14 deletions
diff --git a/doc/PG-adapting.texi b/doc/PG-adapting.texi index c526d2df..27dcb0df 100644 --- a/doc/PG-adapting.texi +++ b/doc/PG-adapting.texi @@ -1918,22 +1918,9 @@ be set non-nil, so that when a completed file is activated for 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}} -should also be set, and will be called immediately after the match. -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 -@defvar proof-done-advancing-require-function -Used in @samp{@code{proof-done-advancing}}, see @samp{@code{proof-shell-require-command-regexp}}.@* -The function is passed the span and the command as arguments. -@end defvar + @node Hooks and other settings @section Hooks and other settings |