aboutsummaryrefslogtreecommitdiffhomepage
path: root/coq
diff options
context:
space:
mode:
authorGravatar Pierre Courtieu <courtieu@lri.fr>2003-02-06 00:07:14 +0000
committerGravatar Pierre Courtieu <courtieu@lri.fr>2003-02-06 00:07:14 +0000
commit7ba3e9f222495aa37c4fca8ab6146941d798ee51 (patch)
tree795b6db5cafa71043bc40802326ec325bb965113 /coq
parent98d56d7e2e01371166b487d4b1a0faeff314f23f (diff)
Slight modification to proof-script-command-end-regexp in coq.el, to
allow command at the end of the buffer.
Diffstat (limited to 'coq')
-rw-r--r--coq/coq.el2
1 files changed, 1 insertions, 1 deletions
diff --git a/coq/coq.el b/coq/coq.el
index ad32135a..473bb31c 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -597,7 +597,7 @@ This is specific to coq-mode."
;;(if coq-version-is-V7 "[.]\\([ \t\n\r]\\)\\|[.]\\'" "[.]")
;; da: could you check this, Pierre? If you like it
;; please remove these comments.
- "[.]\\([\\. \t\n\r]\\)")
+ "[.]\\([\\. \t\n\r\\']\\|\\'\\)")
(setq proof-script-comment-start "(*")
(setq proof-script-comment-end "*)")
(setq proof-unnamed-theorem-name "Unnamed_thm") ; Coq's default name