aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2019-12-09 01:32:10 +0100
committerEmilio Jesus Gallego Arias2019-12-16 10:31:45 +0100
commitbfbcd1e3feeaa7eb24c15686439926c536c5d483 (patch)
treebf97d766e395c7c9c8ffea433e19c1b2476462f1 /dev
parent861a83842efcb536e9ffdd0ba7173621daab47a4 (diff)
[dune] Use a special directory for the boot build
This is related to and fixes #10694 in part. When calling bootstrap in an incremental build step, we must be sure the generated dune files are in place. In the CI, these won't be in place, so we must bootstrap without altering the digest and trace database coming from the artifact. Using a separate boot step to recreate the missing `dune` files works fine and takes just a few seconds.
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions