From f705c67a172c89db899aaface898c159b858ed28 Mon Sep 17 00:00:00 2001
From: Raphael Rieu-Helft <raphael.rieu-helft@lri.fr>
Date: Fri, 22 Jun 2018 14:53:01 +0200
Subject: [PATCH] multiprecision gitattributes

---
 .gitattributes                         | 3 ---
 examples/multiprecision/.gitattributes | 3 +++
 2 files changed, 3 insertions(+), 3 deletions(-)
 create mode 100644 examples/multiprecision/.gitattributes

diff --git a/.gitattributes b/.gitattributes
index 85087c8e0..5cb0f7baf 100644
--- a/.gitattributes
+++ b/.gitattributes
@@ -10,9 +10,6 @@
 
 /bench/encoding/ export-ignore
 /examples/in_progress/ export-ignore
-/examples/multiprecision/random/ export-ignore
-/examples/multiprecision/bench-include/ export-ignore
-/examples/multiprecision/mini-gmp/ export-ignore
 /misc/ export-ignore
 /opam/ export-ignore
 /tests/ export-ignore
diff --git a/examples/multiprecision/.gitattributes b/examples/multiprecision/.gitattributes
new file mode 100644
index 000000000..a179b5909
--- /dev/null
+++ b/examples/multiprecision/.gitattributes
@@ -0,0 +1,3 @@
+random/ export-ignore
+bench-include/ export-ignore
+mini-gmp/ export-ignore
\ No newline at end of file
-- 
GitLab