diff options
Diffstat (limited to '.gitattributes')
| -rw-r--r-- | .gitattributes | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/.gitattributes b/.gitattributes index db179c8d2..e087e1737 100644 --- a/.gitattributes +++ b/.gitattributes @@ -19,6 +19,7 @@ tools/CoqMakefile.in whitespace=trailing-space *.css whitespace=trailing-space,tab-in-indent *.dtd whitespace=trailing-space,tab-in-indent *.el whitespace=trailing-space,tab-in-indent +*.g whitespace=trailing-space,tab-in-indent *.h whitespace=trailing-space,tab-in-indent *.html whitespace=trailing-space,tab-in-indent *.hva whitespace=trailing-space,tab-in-indent @@ -37,9 +38,11 @@ tools/CoqMakefile.in whitespace=trailing-space *.nsh whitespace=trailing-space,tab-in-indent *.nsi whitespace=trailing-space,tab-in-indent *.py whitespace=trailing-space,tab-in-indent +*.rst whitespace=trailing-space,tab-in-indent *.sh whitespace=trailing-space,tab-in-indent *.sty whitespace=trailing-space,tab-in-indent *.tex whitespace=trailing-space,tab-in-indent +*.tokens whitespace=trailing-space,tab-in-indent *.txt whitespace=trailing-space,tab-in-indent *.v whitespace=trailing-space,tab-in-indent *.xml whitespace=trailing-space,tab-in-indent |