aboutsummaryrefslogtreecommitdiffhomepage
path: root/CHANGES
diff options
context:
space:
mode:
authorGravatar Pierre Courtieu <courtieu@lri.fr>2015-03-05 17:35:28 +0000
committerGravatar Pierre Courtieu <courtieu@lri.fr>2015-03-05 17:35:28 +0000
commitbbcee39f5bf8eb74445d4abb78a7aac2ad048cb5 (patch)
tree08927ea32432aeb12f3307389caec3efcf1d09b0 /CHANGES
parent835cc6299c73e75454fbab2f03a3207c86b323de (diff)
Fixed stuff in CHANGES.
Diffstat (limited to 'CHANGES')
-rw-r--r--CHANGES4
1 files changed, 3 insertions, 1 deletions
diff --git a/CHANGES b/CHANGES
index b8fb5e5f..c173e6d2 100644
--- a/CHANGES
+++ b/CHANGES
@@ -32,11 +32,13 @@ the CVS ChangeLog and PG Trac, http://proofgeneral.inf.ed.ac.uk/trac.
Scripting supports bullets of any length.
Indentation supports only bullets of length <= 4 (like ----). Longer
may be supported if needed.
+ For indentation to work well, please use this precedence:
+ - + * -- ++ ** --- +++ *** ...
*** smie indentation is now the only choice.
Old code removed. will work only if emacs >= 23.3.
-*** indentation off modules, sections and proofs are customizable
+*** indentation of modules, sections and proofs are customizable
(setq coq-indent-modulestart X) will set indentation width for
modules and sections to X characters