diff --git a/.gitattributes b/.gitattributes index c925e3166ee66e64206fc6ef05efd4bda052ded0..3781bca8d8c84d92435e3c57e2aa704357f237bd 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