diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 9114ed7f611f8161981c72bfd33c679201511025..d4b55529d40e22d86a86be58fe052b000ffe0a94 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -17,4 +17,5 @@ gps-coq8.6: - coq/opamroot/ only: - master + - /^bench-.*$/ - opam-ci