diff --git a/src/emacs/lean-mode.el b/src/emacs/lean-mode.el index 1d0e50621..5c80c8d25 100644 --- a/src/emacs/lean-mode.el +++ b/src/emacs/lean-mode.el @@ -124,6 +124,7 @@ enabled and disabled respectively.") :syntax-table lean-syntax-table :abbrev-table lean-abbrev-table :group 'lean + (set (make-local-variable 'comment-start) "--") (set (make-local-variable 'comment-start-skip) "[-/]-[ \t]*") (set (make-local-variable 'comment-end) "") (set (make-local-variable 'comment-end-skip) "[ \t]*\\(-/\\|\\s>\\)")