diff options
| author | Emilio Jesus Gallego Arias | 2019-12-09 01:32:10 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-12-16 10:31:45 +0100 |
| commit | bfbcd1e3feeaa7eb24c15686439926c536c5d483 (patch) | |
| tree | bf97d766e395c7c9c8ffea433e19c1b2476462f1 /dev | |
| parent | 861a83842efcb536e9ffdd0ba7173621daab47a4 (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
