From 2f3105f6042484634df883a03477c9c7caf878df Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Thu, 22 Aug 2019 17:57:40 +0200
Subject: [PATCH] [wp] git ignore

---
 src/plugins/wp/share/.gitignore | 18 +++---------------
 1 file changed, 3 insertions(+), 15 deletions(-)

diff --git a/src/plugins/wp/share/.gitignore b/src/plugins/wp/share/.gitignore
index c2552132a1c..b4928767a3a 100644
--- a/src/plugins/wp/share/.gitignore
+++ b/src/plugins/wp/share/.gitignore
@@ -1,18 +1,6 @@
-/ergo/*.mlw.bak
-/why3/why3.conf
-/why3/*.why.bak
-/why3/*.vo
-/why3/*.glob
-/why3/.*.aux
-/why3/.depend
-/coqwp/.depend
-/coqwp/*/*.vo
-/coqwp/*/*.glob
-/coqwp/*.vo
-/coqwp/*.glob
-/coqwp/.*.aux
-/coqwp/*/.*.aux
-/.depend
+*.vo
+*.glob
+*.aux
 /instwp
 /install
 /html
-- 
GitLab