aboutsummaryrefslogtreecommitdiffhomepage
path: root/generic
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2009-08-07 14:10:46 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2009-08-07 14:10:46 +0000
commitac4fe82a0faed262fb2895b2993e4a2c3a2a2fa7 (patch)
tree3b55a4baa1c14fc3d143c21451c931ef7bdce5bf /generic
parent128e2c38c20fef173ad931bbaca3a31b17c9e3db (diff)
rename: proof-full-decoration -> proof-full-annotation
Diffstat (limited to 'generic')
-rw-r--r--generic/proof-menu.el4
1 files changed, 2 insertions, 2 deletions
diff --git a/generic/proof-menu.el b/generic/proof-menu.el
index 4eac1286..ed71aa31 100644
--- a/generic/proof-menu.el
+++ b/generic/proof-menu.el
@@ -297,9 +297,9 @@ without adjusting window layout."
:style toggle
:selected proof-script-fly-past-comments
:help "Coalesce and skip over successive comments"]
- ["Full Decoration" proof-full-decoration-toggle
+ ["Full Annotation" proof-full-annotation-toggle
:style toggle
- :selected proof-full-decoration
+ :selected proof-full-annotation
:help "Record full information to decorate scripts (may cause slowdown)"]
["Disppearing Proofs" proof-disappearing-proofs-toggle
:style toggle