aboutsummaryrefslogtreecommitdiffhomepage
path: root/generic/proof-useropts.el
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2009-09-11 12:03:48 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2009-09-11 12:03:48 +0000
commita12878d837d3c66e98bb0a0b438203a0aca469a9 (patch)
tree38e6ba969e88551645a18dd711373400651e6688 /generic/proof-useropts.el
parent49dd626db18b2a69648d8b25c0e1209baa848ee8 (diff)
Make quiet by default. Improve docs.
Diffstat (limited to 'generic/proof-useropts.el')
-rw-r--r--generic/proof-useropts.el5
1 files changed, 3 insertions, 2 deletions
diff --git a/generic/proof-useropts.el b/generic/proof-useropts.el
index fda3b58d..e4b0b83a 100644
--- a/generic/proof-useropts.el
+++ b/generic/proof-useropts.el
@@ -88,7 +88,7 @@ terminator somewhere nearby. Electric!"
:type 'boolean
:group 'proof-user-options)
-(defcustom proof-shell-quiet-errors nil
+(defcustom proof-shell-quiet-errors t
"If non-nil, be quiet about errors from the prover.
Normally error messages cause a beep. Set this to t to prevent that."
:type 'boolean
@@ -121,7 +121,8 @@ done if this `proof-strict-state-preserving' is turned off (nil)."
(defcustom proof-strict-read-only t
"*Whether Proof General is strict about the read-only region in buffers.
If non-nil, an error is given when an attempt is made to edit the
-read-only region. If nil, Proof General is more relaxed (but may give
+read-only region, except for the special value 'retract which means
+undo first. If nil, Proof General is more relaxed (but may give
you a reprimand!)."
:type '(choice
(const :tag "Do not allow edits" t)