From c0bd5544c6c7dcdef9ddd005c952ea5acf68603b Mon Sep 17 00:00:00 2001
From: Stefan Monnier
Date: Fri, 29 Jun 2012 16:23:50 +0000
Subject: * generic/pg-user.el (which-func-modes): Fix compiler declaration. *
 generic/proof-site.el (assistants): Fix regexp.

---
 generic/proof-script.el | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

(limited to 'generic/proof-script.el')

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
-- 
cgit v1.2.3