diff options
Diffstat (limited to 'generic/proof-script.el')
| -rw-r--r-- | generic/proof-script.el | 10 |
1 files changed, 6 insertions, 4 deletions
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))))) |