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