diff options
author | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-03-31 01:14:26 +0200 |
---|---|---|
committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-03-31 01:14:26 +0200 |
commit | 53ad0fca8fd511da2b457b9b2ec0b8c3c1780b3f (patch) | |
tree | 4cc380185df0e2bc074c78d765fa3bb7974f73a0 | |
parent | 7b9967a1a145ab70181d362ddafeba7ecb0916bd (diff) | |
parent | d73a11c2ec3fda9231baa90e68eb36198f6d22f1 (diff) |
Merge PR #6989: Enable whitespace checking for new Sphinx file extensions.
-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 |