aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile
diff options
context:
space:
mode:
authorGravatar Gaëtan Gilbert <gaetan.gilbert@ens-lyon.fr>2017-05-27 16:00:53 +0200
committerGravatar Gaëtan Gilbert <gaetan.gilbert@ens-lyon.fr>2017-05-28 12:52:55 +0200
commit149b0c422027a31972b62457af1bf97bd016e26c (patch)
tree32f5267f4f24086018d1c04e71a236392f089993 /Makefile
parent2eb27e56ea4764fa2f2acec6f951eef2642ff1be (diff)
Gitlab CI
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile5
1 files changed, 3 insertions, 2 deletions
diff --git a/Makefile b/Makefile
index 7ba2c80f1..d1fa99ccb 100644
--- a/Makefile
+++ b/Makefile
@@ -53,8 +53,9 @@ FIND_VCS_CLAUSE:='(' \
-name 'debian' -o \
-name "$${GIT_DIR}" -o \
-name '_build' -o \
- -name '_build_ci' \
- -name 'coq-makefile' \
+ -name '_build_ci' -o \
+ -name 'coq-makefile' -o \
+ -name '.opamcache' \
')' -prune -o
define find