diff options
| author | Maxime Dénès | 2017-05-29 23:26:23 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-05-29 23:26:23 +0200 |
| commit | 0336d4d19d446315cb922149b8ee4e7885843be0 (patch) | |
| tree | 736e7d580a255d2438a5514ea37b609560bb40a3 /Makefile | |
| parent | 42c752cf0336cbadc8e9c092ff5aed6a38899dda (diff) | |
| parent | 149b0c422027a31972b62457af1bf97bd016e26c (diff) | |
Merge PR#687: Gitlab CI
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 5 |
1 files changed, 3 insertions, 2 deletions
@@ -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 |