aboutsummaryrefslogtreecommitdiffhomepage
path: root/generic/proof-config.el
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2011-10-13 10:59:28 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2011-10-13 10:59:28 +0000
commit8801f39c72c5b88c79ca52655d4591cee7579c69 (patch)
treee804df5ed5d72bf5b80f0a7e7cfd96f51e6a91eb /generic/proof-config.el
parent61f0ddc231bdccec08547a3d824cef41eeceadb3 (diff)
To fix pgshell mode, restore proof-shell-insert support for a single string argument and allow nil setting for proof-shell-start-goals-regexp.
Diffstat (limited to 'generic/proof-config.el')
-rw-r--r--generic/proof-config.el3
1 files changed, 2 insertions, 1 deletions
diff --git a/generic/proof-config.el b/generic/proof-config.el
index 92b24db1..c5a49340 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -1148,7 +1148,8 @@ is shown to the user. Set to nil to disable."
"Regexp matching the start of the proof state output.
This is an important setting. Output between `proof-shell-start-goals-regexp'
and `proof-shell-end-goals-regexp' will be pasted into the goals buffer
-and possibly analysed further for proof-by-pointing markup."
+and possibly analysed further for proof-by-pointing markup.
+If it is left as nil, the goals buffer will not be used."
:type '(choice nil regexp)
:group 'proof-shell)