aboutsummaryrefslogtreecommitdiff
path: root/CHANGES
diff options
context:
space:
mode:
authorDavid Aspinall2009-09-06 14:02:15 +0000
committerDavid Aspinall2009-09-06 14:02:15 +0000
commit99d21e5c443ddbd1e773f1ef4baf2e9a6fe7b78c (patch)
tree52ac691dd1899895e3605cbfcb53988044aab784 /CHANGES
parent594f3c0e21e9064bce8bb04750d7595cfefae705 (diff)
Remove use-specials-for-fontify
Diffstat (limited to 'CHANGES')
-rw-r--r--CHANGES3
1 files changed, 2 insertions, 1 deletions
diff --git a/CHANGES b/CHANGES
index 53458b4a..fc7e6c34 100644
--- a/CHANGES
+++ b/CHANGES
@@ -36,10 +36,11 @@
proof-toolbar-use-button-enablers (now always used)
proof-output-fontify-enable (now always enabled)
-*** Altered prover configuration settings
+*** Altered prover configuration settings (internal)
pg-insert-output-as-comment-fn: removed
proof-shell-wakeup-char: removed
proof-shell-prompt-pattern: removed
+ 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