merge idris master

This commit is contained in:
Barak Michener 2018-01-09 00:44:34 -08:00
parent ee43fabed2
commit 0bbef95663
3 changed files with 17 additions and 11 deletions

View file

@ -89,6 +89,10 @@ augroup go
autocmd FileType go nmap gd <Plug>(go-def)
augroup END
augroup idris
autocmd FileType idris nmap <LocalLeader>a a?hole<Esc><LocalLeader>t
augroup end
autocmd FileType go let b:auto_trim_whitespace=1
autocmd FileType cpp let b:auto_trim_whitespace=1
autocmd FileType perl let b:auto_trim_whitespace=1
@ -97,4 +101,6 @@ autocmd FileType javascript let b:auto_trim_whitespace=1
autocmd FileType python let b:auto_trim_whitespace=1
autocmd FileType proto let b:auto_trim_whitespace=1
autocmd FileType hy let b:auto_trim_whitespace=1
autocmd FileType idris let b:auto_trim_whitespace=1
autocmd FileType java let b:auto_trim_whitespace=1