diff options
| author | Gaëtan Gilbert | 2019-07-15 13:15:35 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-07-15 13:15:35 +0200 |
| commit | c69843ff2ba3f6e8b5f9d04ad3b01a4ccf9ad9c0 (patch) | |
| tree | a719deddae89629f863319f6ea9de84b899bdc8b | |
| parent | 76dfd0b95a7fd2de99f65de9fc10925d58777cd4 (diff) | |
Azure CI MacOS: build byte target first
It looks like the recent spurious failures are because it somehow
wants to build gramlib byte and opt at the same time and the old race
condition causes the error.
Having failed to debug the makefile, we work around by building byte first.
| -rw-r--r-- | azure-pipelines.yml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/azure-pipelines.yml b/azure-pipelines.yml index fd99dc6d18..1648638555 100644 --- a/azure-pipelines.yml +++ b/azure-pipelines.yml @@ -81,6 +81,7 @@ jobs: eval $(opam env) ./configure -prefix '$(Build.BinariesDirectory)' -warn-error yes -native-compiler no -coqide opt + make -j "$NJOBS" byte make -j "$NJOBS" displayName: 'Build Coq' |