From 2ebe75bf0ae077ada07ed4d42ef2c4bd2f9562ee Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 6 Oct 2017 23:50:42 +0200
Subject: [PATCH] stop excluding files from git exports

---
 .gitattributes | 2 --
 1 file changed, 2 deletions(-)
 delete mode 100644 .gitattributes

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