diff options
| author | Emilio Jesus Gallego Arias | 2018-11-18 17:39:57 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-11-24 13:16:00 +0100 |
| commit | c8dd2b51e413ae1522b6278e36b5e56e0f9a5585 (patch) | |
| tree | de0c04d460b999d0520327cf9bdab7968d9e7e28 /dev/ci/README-users.md | |
| parent | 991790c8135cf3073907fda3baadc9718419f173 (diff) | |
[ci] [doc] Note about `overlay-maintainers` team.
Diffstat (limited to 'dev/ci/README-users.md')
| -rw-r--r-- | dev/ci/README-users.md | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/dev/ci/README-users.md b/dev/ci/README-users.md index 2b400f4136..f606f43fd5 100644 --- a/dev/ci/README-users.md +++ b/dev/ci/README-users.md @@ -33,6 +33,18 @@ would be moved into our "allow failure" category. At the end of the grace period, in the absence of progress, the development would be removed from our CI. +### Timely merging of overlays + +A pitfall of the current CI setup is that when a breaking change is +merged in Coq upstream, CI for your contrib will be broken until you +merge the corresponding pull request with the fix for your contribution. + +As of today, you have to worry about synchronizing with Coq upstream +every once in a while; we hope we will improve this in the future by +using [coqbot](https://github.com/coq/bot); meanwhile, a workaround is +to give merge permissions to someone from the Coq team as to help with +these kind of merges. + ### Add your development by submitting a pull request Add a new `ci-mydev.sh` script to [`dev/ci`](.); set the corresponding |