From a8be1e2551bc4fbda9c45792c0dad5743c18fefd Mon Sep 17 00:00:00 2001
From: Columbus240
Date: Mon, 24 Aug 2020 19:27:33 +0200
Subject: Merge some of the gitignore files

Both /.gitignore and /lib/coq/.gitignore ignored some files in /lib/coq.
This commit removes /lib/coq/.gitignore and moves all ignore-statements
to /.gitignore . This should simplify the maintenance of gitignore files.

The situation with /test/mono/.gitignore is analogous.
---
 lib/coq/.gitignore | 1 -
 1 file changed, 1 deletion(-)
 delete mode 100644 lib/coq/.gitignore

(limited to 'lib')

diff --git a/lib/coq/.gitignore b/lib/coq/.gitignore
deleted file mode 100644
index 1aa62803..00000000
--- a/lib/coq/.gitignore
+++ /dev/null
@@ -1 +0,0 @@
-deps
\ No newline at end of file
-- 
cgit v1.2.3