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-developers.md | |
| parent | 991790c8135cf3073907fda3baadc9718419f173 (diff) | |
[ci] [doc] Note about `overlay-maintainers` team.
Diffstat (limited to 'dev/ci/README-developers.md')
| -rw-r--r-- | dev/ci/README-developers.md | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/dev/ci/README-developers.md b/dev/ci/README-developers.md index 8cb1a0edef..54da7a7cd3 100644 --- a/dev/ci/README-developers.md +++ b/dev/ci/README-developers.md @@ -72,7 +72,7 @@ Moreover your PR must absolutely update the [`CHANGES.md`](../../CHANGES.md) fil If you break external projects that are hosted on GitHub, you can use the `create-overlays.sh` script to automatically perform most of the -above step. In order to do so, call the script as: +above steps. In order to do so, call the script as: ``` ./dev/tools/create-overlays.sh ejgallego 9873 aac_tactics elpi ltac ``` @@ -81,7 +81,7 @@ number. The script will: - checkout the contributions and prepare the branch/remote so you can just commit the fixes and push, -- add the corresponding overlay file in `dev/ci/user-overlays` +- add the corresponding overlay file in `dev/ci/user-overlays`. For problems related to ML-plugins, if you use `dune build` to build Coq, it will actually be aware of the broken contributions and perform |