diff options
| author | Emilio Jesus Gallego Arias | 2018-10-08 17:59:13 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-10-08 17:59:13 +0200 |
| commit | 6609b8b1ea9ab96dbe7b510b92bf7b5d4b81b210 (patch) | |
| tree | 683e0900d9e77c24fc87a290d8da0ac21b076d20 /dev/ci/ci-basic-overlay.sh | |
| parent | 2de0af56b813f2004261eb15fe22586105f3c886 (diff) | |
[dune] Fix bad interaction among PR #8627 and #8657
Dangers of not stacking PRs hit again, and here we hit a problem
breaking the build on master due to #8627 adding a new file to install
with for the (implicit) `coq` package and #8657 removing the implicit
status of such package.
Diffstat (limited to 'dev/ci/ci-basic-overlay.sh')
0 files changed, 0 insertions, 0 deletions