diff options
| author | Michael Soegtrop | 2018-10-05 11:39:22 +0200 |
|---|---|---|
| committer | Michael Soegtrop | 2018-10-05 14:07:06 +0200 |
| commit | 4bd1bb0091d2e69637444b776f6025a4b1c049b7 (patch) | |
| tree | 31dcfe0bef30f8bfa1c4ae62321d39e6de16832d /dev/ci/README.md | |
| parent | d3bfed08d0e53e953fca996e72adf0dc4f132f98 (diff) | |
Fix issue #8659 - Not always build extended set of addons for Windows installer
Diffstat (limited to 'dev/ci/README.md')
| -rw-r--r-- | dev/ci/README.md | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/dev/ci/README.md b/dev/ci/README.md index 24952eb5b7..47ce0cb060 100644 --- a/dev/ci/README.md +++ b/dev/ci/README.md @@ -178,6 +178,11 @@ versions of Coq (32bit and 64bit). The Windows jobs are enabled on Coq's repository, where pipelines for pull requests run. +If the additional secret variable `WINDOWS_ALL_ADDONS` is set to `enabled`, +an extended set of addons will be added to the Windows installer. +This leads to a considerable runtime in CI and is disabled by default for +pipelines for pull requests. + ### GitLab and Docker System and opam packages are installed in a Docker image. The image is |