diff --git a/.gitattributes b/.gitattributes deleted file mode 100644 index 6ab3d923c22eb279d761d7ef31e424e533cb77a9..0000000000000000000000000000000000000000 --- a/.gitattributes +++ /dev/null @@ -1,2 +0,0 @@ -opam export-ignore -.git* export-ignore