diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2009-09-08 23:11:19 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2009-09-08 23:11:19 +0000 |
| commit | 99144e61c6dc666ddbab17ebb9b90798b52c7631 (patch) | |
| tree | 738c4bce2ac96d8d0c0703ca7de251c4d911d369 /generic/proof-config.el | |
| parent | 20b779d49151095bab6b235538f12ef8f60b2fff (diff) | |
proof-kill-goal-command: default to nil, not empty string
Diffstat (limited to 'generic/proof-config.el')
| -rw-r--r-- | generic/proof-config.el | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/generic/proof-config.el b/generic/proof-config.el index a4b9bb0f..41a5b5e9 100644 --- a/generic/proof-config.el +++ b/generic/proof-config.el @@ -648,7 +648,7 @@ will be attempted." :type '(choice function nil) :group 'proof-script) -(defcustom proof-kill-goal-command "" +(defcustom proof-kill-goal-command nil "Command to kill the currently open goal. If this is set to nil, PG will expect `proof-find-and-forget-fn' @@ -1667,7 +1667,7 @@ Plastic uses it to remove literate-style markup from `string'." (defcustom proof-shell-handle-error-or-interrupt-hook '(proof-goto-end-of-locked-on-error-if-pos-not-visible-in-window) "Run after an error or interrupt has been reported in the response buffer. -Hook functions may inspect `proof-shell-error-or-interrupt-seen' to +Hook functions may inspect `proof-shell-last-output-kind' to determine whether the cause was an error or interrupt. Possible values for this hook include: |