aboutsummaryrefslogtreecommitdiff
path: root/.gitattributes
diff options
context:
space:
mode:
authorVincent Laporte2019-05-06 13:08:14 +0000
committerVincent Laporte2019-05-06 13:08:14 +0000
commit1a670a23ad54cf5a3c2d2bbf4939f78f4f4b6b35 (patch)
tree81288272de52b007499b1d8d5933aad508c1660a /.gitattributes
parent6ff10c569c1684927d4cb866a159fe6f54e55abe (diff)
parent50b148154fada66bb1145aaba696d9b427511592 (diff)
Merge PR #9964: Unreleased changelog folder
Ack-by: SkySkimmer Ack-by: Zimmi48 Reviewed-by: gares Reviewed-by: vbgl
Diffstat (limited to '.gitattributes')
-rw-r--r--.gitattributes1
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