From c46355d3400389ad347e58036de408b678f0c3ea Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Thu, 13 Jun 2002 10:59:04 +0000
Subject: Docs

---
 generic/proof-config.el | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

(limited to 'generic')

diff --git a/generic/proof-config.el b/generic/proof-config.el
index f54363a4..dd1d05b4 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -1261,7 +1261,14 @@ will be attempted."
 
 (defcustom proof-kill-goal-command ""
   "Command to kill the currently open goal.
-You must set this (perhaps to a no-op) for script management to work."
+If this is set to nil, PG will expect proof-find-and-forget-fn
+to do all the work of retracting to an arbitrary point in a file.
+Otherwise, the generic split-phase mechanism will be used:
+
+  1. If inside an unclosed proof, use proof-count-undos.
+  2. If retracting to before an unclosed proof, use 
+     proof-kill-goal-command, followed by proof-find-and-forget-fn
+     if necessary."
   :type 'string
   :group 'proof-script)
 
-- 
cgit v1.2.3