Merge branch 'master' of github.com:edwinb/Idris-dev
commit649330f9fa2ee561cd17a2056f14cc1fc6bbad55
authorEdwin Brady <ecb10@st-andrews.ac.uk>
dateWed 10 Apr 2013, 10:28 (14 years ago)
parent03f962a17b9f43
contribs/tool-support/vim/ftplugin/idris.vim+3−3
@@ -1,3 +1,3 @@
1−set shiftwidth=2
2−set tabstop=2
3−set expandtab
1+setlocal shiftwidth=2
2+setlocal tabstop=2
3+setlocal expandtab