diff options
| author | Emilio Jesus Gallego Arias | 2018-06-12 14:56:57 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-06-12 14:56:57 +0200 |
| commit | d4dd162526c47c2d5fc99423409a25e49473dc15 (patch) | |
| tree | 7104269cff61cbebd2ea61dc668cf74bdf8c832f /dev/header.ml | |
| parent | 7e7aa7491e3743abe858c1be6b77bd9a986d4297 (diff) | |
[ci] Require runner `docker` tag on `docker-boot` job.
Not all runners are equipped with docker services, thus we must add a
hard dependency on the `docker` tag for our Docker job.
Diffstat (limited to 'dev/header.ml')
0 files changed, 0 insertions, 0 deletions