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 /lib | |
| 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.
Diffstat (limited to 'lib')
0 files changed, 0 insertions, 0 deletions