diff options
| author | Emilio Jesus Gallego Arias | 2019-08-23 20:47:39 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-12-16 10:31:42 +0100 |
| commit | 861a83842efcb536e9ffdd0ba7173621daab47a4 (patch) | |
| tree | a14a65f685f03150d191ee91e95d03da2fa4bccc /.gitignore | |
| parent | df12d00bd01801088b6b8c50e51142e646053829 (diff) | |
[ci] [dune] Updates to dune builds artifacts.
Closes #10694
We modify handling of artifacts for dune builds:
- we preserve `_build/log` log as artifact for ci-builds,
- we use a tar.gz as to preserve file permissions which is necessary
in order to reuse the artifacts in an incremental build.
Dune uses this rule to digest a file:
```
Digest.generic (file_contents f, f.stats.st_perm land 0o100 (* Only take USR_X in account *))
```
Since a few releases, Gitlab CI uses `.zip` as the storage format for
artifacts, this means that files in `_build` will get the executable
bit set when they did not have it originally, making all the digest
cache to miss. This caused #10694 .
See https://gitlab.com/gitlab-org/gitlab/issues/18711
Diffstat (limited to '.gitignore')
0 files changed, 0 insertions, 0 deletions
