aboutsummaryrefslogtreecommitdiffhomepage
path: root/CHANGES
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2012-08-14 10:37:25 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2012-08-14 10:37:25 +0000
commitcaf7542b618ef6e39853613733c5aa7d4607f224 (patch)
treeb130d13cc2d5fe9cb6749cba24eebc1576344c41 /CHANGES
parentcdacdc30c3708e1a824ada65584f6d6a5a4bc03d (diff)
Add user option proof-next-command-insert-space.
Diffstat (limited to 'CHANGES')
-rw-r--r--CHANGES7
1 files changed, 7 insertions, 0 deletions
diff --git a/CHANGES b/CHANGES
index b842ccf3..a5dae661 100644
--- a/CHANGES
+++ b/CHANGES
@@ -8,6 +8,11 @@ the CVS ChangeLog and PG Trac, http://proofgeneral.inf.ed.ac.uk/trac.
** Generic/misc changes
+*** Added user option: `proof-next-command-insert-space'
+ Allows the user to turn off the electric behaviour of generating
+ newlines or spaces in the buffer. Turned on by default, set
+ to nil to revert to PG 3.7 behaviour.
+
*** Support proof-tree visualization via the external Prooftree program
Currently only Coq (using Coq version 8.4beta or newer)
supports proof-tree visualization. If Prooftree is installed,
@@ -18,6 +23,8 @@ the CVS ChangeLog and PG Trac, http://proofgeneral.inf.ed.ac.uk/trac.
*** Compilation fixes for Emacs 24.
*** Fix "pgshell" mode for shell/CLI prover interaction
+ Also add some quick hacks for scripting OCaml and Haskell
+
** Coq changes