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 /.gitignore | |
| 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 '.gitignore')
| -rw-r--r-- | .gitignore | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/.gitignore b/.gitignore index 6c117028a9..12a5c11e5e 100644 --- a/.gitignore +++ b/.gitignore @@ -52,6 +52,7 @@ TAGS bin/ _build_ci _build +_build_boot config/Makefile config/coq_config.ml config/coq_config.py |