aboutsummaryrefslogtreecommitdiffhomepage
path: root/generic/proof-script.el
diff options
context:
space:
mode:
authorGravatar Stefan Monnier <monnier@iro.umontreal.ca>2012-06-29 16:23:50 +0000
committerGravatar Stefan Monnier <monnier@iro.umontreal.ca>2012-06-29 16:23:50 +0000
commitc0bd5544c6c7dcdef9ddd005c952ea5acf68603b (patch)
treebeec5fbedb963cd7b0eef0d1335a26c76b37ad1f /generic/proof-script.el
parentec00c7fe67dc27c13b6b7bab42d60feb66355240 (diff)
* generic/pg-user.el (which-func-modes): Fix compiler declaration.
* generic/proof-site.el (assistants): Fix regexp.
Diffstat (limited to 'generic/proof-script.el')
-rw-r--r--generic/proof-script.el6
1 files changed, 5 insertions, 1 deletions
diff --git a/generic/proof-script.el b/generic/proof-script.el
index 74e92918..4ddb0045 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -2390,7 +2390,11 @@ assistant."
(regexp-quote "\n") ;; end-of-line terminated comments
(regexp-quote proof-script-comment-end))))
- ;; BOGUS
+ ;; FIXME: This is clearly bogus: it sets the *start* matcher based on the
+ ;; *end* marker. But I'm not sure what's the right fix: OT1H the code is
+ ;; careful to build a correct end-matcher, but OTOH it's not as careful as
+ ;; the default code in newcomment.el anyway. So I'm tempted to just remove
+ ;; this code altogether.
(make-local-variable 'comment-start-skip)
(unless comment-start-skip
(setq comment-start-skip