diff options
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 |