From 3a41dad60aeed83ea6c3ece9e1721c0d913dba9f Mon Sep 17 00:00:00 2001 From: Ralf Jung <jung@mpi-sws.org> Date: Fri, 4 Jun 2021 12:45:54 +0200 Subject: [PATCH] sync gitattributes with std++ --- .gitattributes | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/.gitattributes b/.gitattributes index c925e3166..3781bca8d 100644 --- a/.gitattributes +++ b/.gitattributes @@ -1 +1,6 @@ *.v gitlab-language=coq + +# Convert to native line endings on checkout. +*.ref text +# Shell scripts need Linux line endings. +*.sh eol=lf -- GitLab