From 1f0e449835faf3e5676480595db2f9e949bcbdc3 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 31 Oct 2019 14:01:52 +0100
Subject: [PATCH] treat .ref files with native line endings

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

diff --git a/.gitattributes b/.gitattributes
index c925e316..258cd319 100644
--- a/.gitattributes
+++ b/.gitattributes
@@ -1 +1,5 @@
+# Enable syntax highlighting.
 *.v gitlab-language=coq
+
+# Convert to native line endings on checkout.
+*.ref text
-- 
GitLab