diff options
| author | Emilio Jesus Gallego Arias | 2018-03-31 01:14:26 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 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 db179c8d20..e087e17379 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 |
