aboutsummaryrefslogtreecommitdiffhomepage
path: root/generic/proof-script.el
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2009-09-14 22:08:31 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2009-09-14 22:08:31 +0000
commitfae9a2a46ee5def106e5afb8e3facc6120191012 (patch)
tree84dd98a2507721f5b43adaead41f349f816bdd17 /generic/proof-script.el
parent3f7859567fd9159daf7050fda3f5cfb57052470f (diff)
proof-span-give-warning: no message if inhibit-read-only is set
Diffstat (limited to 'generic/proof-script.el')
-rw-r--r--generic/proof-script.el3
1 files changed, 2 insertions, 1 deletions
diff --git a/generic/proof-script.el b/generic/proof-script.el
index 97ffbf8d..7472743b 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -131,7 +131,8 @@ scripting buffer may have an active queue span.")
(defun proof-span-give-warning (&rest args)
"Give a warning message.
Optional argument ARGS is ignored."
- (message "You should not edit here!"))
+ (unless inhibit-read-only
+ (message "You should not edit here!")))
(defun proof-span-read-only (span &optional always)
"Make SPAN read-only, following variable `proof-strict-read-only' or ALWAYS."