diff options
| author | Théo Zimmermann | 2019-04-27 16:29:04 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2019-04-27 16:29:12 +0200 |
| commit | 93febec88b7e839f9b651a01ab3e3d41b312074e (patch) | |
| tree | cfb3a9fa345ad0be285199ca7c4d133d1809f336 | |
| parent | ae4239d6a5f4afcd9b7321dba790ffd4a64994a1 (diff) | |
[ci/gitlab] Remove after_switch message (not useful anymore).
This was put in place for @coqbot to detect runner failures, but now
the strategy is different.
| -rw-r--r-- | .gitlab-ci.yml | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 3c427793e2..5fa41bb9f7 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -47,9 +47,6 @@ before_script: - opam list - opam config list -after_script: - - echo "The build completed normally (not a runner failure)." - ################ GITLAB CACHING ###################### # - use artifacts between jobs # ###################################################### |