aboutsummaryrefslogtreecommitdiff
path: root/.gitattributes
AgeCommit message (Expand)Author
2019-07-19Introduce doc_gram, a utilty for extracting Coq's grammar from .mlg filesJim Fehrle
2019-05-05Create categories in changelog.Théo Zimmermann
2019-02-26Fix gitattributes for Makefile.duneGaëtan Gilbert
2019-02-20Enable whitespace checking for some forgotten files.Gaëtan Gilbert
2018-12-20Fix line ending issuesGaëtan Gilbert
2018-12-17Fix git line ending conversion in windowsGaëtan Gilbert
2018-06-04Make whitespace linter not check for trailing newlines.Gaëtan Gilbert
2018-03-13Enable whitespace checking for new Sphinx file extensions.Gaëtan Gilbert
2018-03-01Harden gitattributes against core.whitespace configuration.Gaëtan Gilbert
2017-11-20Disable whitespace linter for .out files.Gaëtan Gilbert
2017-10-25Add linter.Gaëtan Gilbert
2017-10-05Shorten the .gitattributes file.Théo Zimmermann
2015-03-16gitattributes: add `.mailmap` file to the list of files excluded from the `.t...Arnaud Spiwack
2015-03-16Gitattributes file added to generate archive.Guillaume Claret
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 06:48:04 +0000