From 9349e0367d2d50b11ccd31c8f6d1979ebd52e555 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 14 Dec 2018 16:11:39 +0100
Subject: Fix git line ending conversion in windows

---
 .gitattributes | 3 +++
 1 file changed, 3 insertions(+)

(limited to '.gitattributes')

diff --git a/.gitattributes b/.gitattributes
index a5edcdb5bf..742ef27f49 100644
--- a/.gitattributes
+++ b/.gitattributes
@@ -53,3 +53,6 @@ tools/CoqMakefile.in whitespace=blank-at-eol
 
 # CR is desired for these Windows files.
 *.bat whitespace=cr-at-eol,blank-at-eol,tab-in-indent
+
+* eol=lf
+*.bat eol=crlf
-- 
cgit v1.2.3