diff options
| author | Erik Martin-Dorel | 2019-07-30 16:49:28 +0200 |
|---|---|---|
| committer | Erik Martin-Dorel | 2019-07-30 16:56:45 +0200 |
| commit | 5bccaf10977a1cb86e00fc2e986bfbe1ac86ad1b (patch) | |
| tree | 19b4cd5a8dabf4f305451a3b95501942c791cbb5 /docs/stylesheets | |
| parent | d5ac333d1ee1b4f3a8d38dc0238c661dcc4a89f7 (diff) | |
[ci] Adapt the GitLab CI config to allow scheduled builds for coq-dev
* Normal builds (branches & GitHub PRs) are not impacted
* Triggering a scheduled pipeline will only run {coq-dev, mathcomp-dev:coq-dev}
to build and deploy the corresponding image to mathcomp/mathcomp-dev:coq-dev.
* href: https://docs.gitlab.com/ce/user/project/pipelines/schedules.html
Diffstat (limited to 'docs/stylesheets')
0 files changed, 0 insertions, 0 deletions