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