From d985cda3b7142b09b84e9daad67c8d2f82e59495 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Tue, 6 Apr 2004 16:11:46 +0000
Subject: Adjust proof-script-comment-end to fix comment-end to be empty for
 end-of-line comments.

---
 generic/proof-script.el | 12 ++++++++++--
 1 file changed, 10 insertions(+), 2 deletions(-)

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

diff --git a/generic/proof-script.el b/generic/proof-script.el
index 7ee34569..0d14f43f 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -2527,12 +2527,20 @@ assistant."
   (make-local-variable 'comment-start)
   (setq comment-start (concat proof-script-comment-start " "))
   (make-local-variable 'comment-end)
-  (setq comment-end (concat " " proof-script-comment-end))
+  (setq comment-end
+	;; For end of line terminated comments, stays empty.
+	(if (string-equal "" proof-script-comment-end)
+	    ""
+	  ;; Otherwise, an extra space before comment delimiter
+	  (concat " " proof-script-comment-end)))
   
   (unless proof-script-comment-start-regexp
     (setq proof-script-comment-start-regexp (regexp-quote proof-script-comment-start)))
   (unless proof-script-comment-end-regexp
-    (setq proof-script-comment-end-regexp (regexp-quote proof-script-comment-end)))
+    (setq proof-script-comment-end-regexp 
+	  (if (string-equal "" proof-script-comment-end)
+	      (regexp-quote "\n") ;; end-of-line terminated comments
+	    (regexp-quote proof-script-comment-end))))
 
   (make-local-variable 'comment-start-skip)
   (setq comment-start-skip
-- 
cgit v1.2.3