diff options
| author | Théo Zimmermann | 2019-04-30 11:42:23 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2019-05-05 19:23:27 +0200 |
| commit | 81301b55df9c52fe5503421eb9527bb04a1643e0 (patch) | |
| tree | 14cf08848ff1178e150d713c3a41386843d974b4 /.gitattributes | |
| parent | 30d6ffdd4546d56c517bef5b31a862c5454240f0 (diff) | |
Create categories in changelog.
Diffstat (limited to '.gitattributes')
| -rw-r--r-- | .gitattributes | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/.gitattributes b/.gitattributes index 58b1a31d36..260e3f96b6 100644 --- a/.gitattributes +++ b/.gitattributes @@ -54,6 +54,7 @@ dune* whitespace=blank-at-eol,tab-in-indent .gitattributes whitespace=blank-at-eol,tab-in-indent _CoqProject whitespace=blank-at-eol,tab-in-indent Dockerfile whitespace=blank-at-eol,tab-in-indent +00000-title.rst -whitespace # tabs are allowed in Makefiles. Makefile* whitespace=blank-at-eol |