From a65f4b532fe1611aaecb19334ac5cc6671d83b9f Mon Sep 17 00:00:00 2001
From: Pierre Courtieu
Date: Sat, 9 Jun 2012 12:58:56 +0000
Subject: Made a small change in generic code about the setting of
 comment-start-skip: if it is already set then proof-script should not change
 it. Ultimately if David approves we should moreover fix the setting itself
 which is bugged. coq-mode now sets this variable by itself.

---
 coq/coq.el              |  5 +++++
 generic/proof-script.el | 10 ++++++----
 2 files changed, 11 insertions(+), 4 deletions(-)

diff --git a/coq/coq.el b/coq/coq.el
index de331372..97b9943a 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -1271,6 +1271,11 @@ This is specific to `coq-mode'."
   (setq proof-script-parse-function 'coq-script-parse-function)
   (setq proof-script-comment-start "(*")
   (setq proof-script-comment-end "*)")
+  (make-local-variable 'comment-start-skip)
+  (setq comment-start-skip
+        (if (string-equal "" proof-script-comment-start)
+            (regexp-quote "\n") ;; end-of-line terminated comments
+          (regexp-quote proof-script-comment-start)))
   (setq proof-unnamed-theorem-name "Unnamed_thm") ; Coq's default name
 
   (setq proof-assistant-home-page coq-www-home-page)
diff --git a/generic/proof-script.el b/generic/proof-script.el
index 9a9d4042..74e92918 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -2390,11 +2390,13 @@ assistant."
 	      (regexp-quote "\n") ;; end-of-line terminated comments
 	    (regexp-quote proof-script-comment-end))))
 
+  ;; BOGUS
   (make-local-variable 'comment-start-skip)
-  (setq comment-start-skip
-	(if (string-equal "" proof-script-comment-end)
-	    (regexp-quote "\n") ;; end-of-line terminated comments
-	  (regexp-quote proof-script-comment-end))))
+  (unless comment-start-skip
+    (setq comment-start-skip
+	  (if (string-equal "" proof-script-comment-end)
+	      (regexp-quote "\n") ;; end-of-line terminated comments
+	    (regexp-quote proof-script-comment-end)))))
 
 
 
-- 
cgit v1.2.3