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 +++++ 1 file changed, 5 insertions(+) (limited to 'coq/coq.el') 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) -- cgit v1.2.3