From abf6968d6caf01aeec41b41b6b6add1b8bc753f4 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Fri, 7 Jul 2017 13:30:15 +0200
Subject: [PATCH] Add .gitattribute to ignore some files during the export.

---
 .gitattribute | 2 ++
 1 file changed, 2 insertions(+)
 create mode 100644 .gitattribute

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