aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorDavid Aspinall2009-09-08 21:06:29 +0000
committerDavid Aspinall2009-09-08 21:06:29 +0000
commitf0bef2c0938b4f56a4b487d154623f0c368a18c9 (patch)
tree7347bafb929dd6f50f9a30e93f919fe1db8567a9
parentaff2ea4bbb63aff1a85b759e5541e3b7683d9776 (diff)
Update, remove proof-shell-abort-goal-regexp
-rw-r--r--CHANGES7
1 files changed, 4 insertions, 3 deletions
diff --git a/CHANGES b/CHANGES
index c55c1f18..e8aea558 100644
--- a/CHANGES
+++ b/CHANGES
@@ -42,9 +42,10 @@
`proof-shell-clear-response-regexp', etc, must match
strings which begin with `proof-shell-eager-annotation-start'.
- pg-insert-output-as-comment-fn: removed
- proof-shell-wakeup-char: removed
- proof-shell-prompt-pattern: removed
+ pg-insert-output-as-comment-fn: removed (use p-s-last-output)
+ proof-shell-wakeup-char: removed (special chars deprecated)
+ proof-shell-prompt-pattern: removed (was only for shell UI)
+ proof-shell-abort-goal-regexp: removed (ordinary response)
pg-use-specials-for-fontify: removed
proof-shell-strip-output-markup: required for cut-and-paste
proof-electric-terminator-noterminator: allows non-insert of terminator