aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--.gitattributes1
-rw-r--r--.gitignore5
2 files changed, 6 insertions, 0 deletions
diff --git a/.gitattributes b/.gitattributes
new file mode 100644
index 0000000..e4504cf
--- /dev/null
+++ b/.gitattributes
@@ -0,0 +1 @@
+.git* export-ignore
diff --git a/.gitignore b/.gitignore
index e176c39..d10613b 100644
--- a/.gitignore
+++ b/.gitignore
@@ -12,3 +12,8 @@ mathcomp/ssreflect/ssreflect.ml4
mathcomp/ssreflect/ssrmatching.ml4
mathcomp/ssreflect/ssrmatching.mli
mathcomp/ssreflect/ssreflect.mllib
+mathcomp/ssreflect.ml4
+mathcomp/ssrmatching.ml4
+mathcomp/ssrmatching.mli
+mathcomp/ssreflect.mllib
+mathcomp-*.tar.gz