michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(emacs/lean-mode): add comment-start "--"

Browse source 
fix #113
This commit is contained in:
Soonho Kong 2014-08-29 20:08:29 -07:00
parent 59d3227eaa
commit 543fdf840e
1 changed files with 1 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/emacs/lean-mode.el
View file

@ -124,6 +124,7 @@ enabled and disabled respectively.")
:syntax-table lean-syntax-table :syntax-table lean-syntax-table
:abbrev-table lean-abbrev-table :abbrev-table lean-abbrev-table
:group 'lean :group 'lean
(set (make-local-variable 'comment-start) "--")
(set (make-local-variable 'comment-start-skip) "[-/]-[ \t]*") (set (make-local-variable 'comment-start-skip) "[-/]-[ \t]*")
(set (make-local-variable 'comment-end) "") (set (make-local-variable 'comment-end) "")
(set (make-local-variable 'comment-end-skip) "[ \t]*\\(-/\\|\\s>\\)") (set (make-local-variable 'comment-end-skip) "[ \t]*\\(-/\\|\\s>\\)")