aboutsummaryrefslogtreecommitdiffhomepage
path: root/CHANGES
diff options
context:
space:
mode:
authorGravatar Pierre Courtieu <Pierre.Courtieu@cnam.fr>2016-07-22 18:34:09 +0200
committerGravatar Pierre Courtieu <Pierre.Courtieu@cnam.fr>2016-07-22 18:34:09 +0200
commit68b82cd171404f0b5ecd5fc699d0931d5a03345c (patch)
tree3ed9b37a9a367edfc962f0b84aaa3c7ec6b96095 /CHANGES
parentc302c243bbb31c22c239ebc6574db61b5b16145a (diff)
Adding the option to highlight susual symbols.
This may look ugly to the majority, so I let it off by default. I find it helpfull to have structuring symbols bold.
Diffstat (limited to 'CHANGES')
-rw-r--r--CHANGES5
1 files changed, 3 insertions, 2 deletions
diff --git a/CHANGES b/CHANGES
index a1119369..77d25277 100644
--- a/CHANGES
+++ b/CHANGES
@@ -142,8 +142,9 @@ the GIT ChangeLog and PG Trac, http://proofgeneral.inf.ed.ac.uk/trac.
*** Removed the Set Undo 500 at start.
This is obsolete. To recover: (setq coq-user-init-cmd `("Set Undo 500."))
-
-
+*** Option to highlight usual symbols
+ Off by default, enable using:
+ (setq coq-symbol-highlight-enable t)
**** Minibuffer interactive queries