aboutsummaryrefslogtreecommitdiff
path: root/.gitignore
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2019-08-23 20:47:39 +0200
committerEmilio Jesus Gallego Arias2019-12-16 10:31:42 +0100
commit861a83842efcb536e9ffdd0ba7173621daab47a4 (patch)
treea14a65f685f03150d191ee91e95d03da2fa4bccc /.gitignore
parentdf12d00bd01801088b6b8c50e51142e646053829 (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