diff options
| author | Guillaume Melquiond | 2018-10-05 08:38:17 +0200 |
|---|---|---|
| committer | Guillaume Melquiond | 2018-10-05 08:38:17 +0200 |
| commit | 6f56c46a8b2383c4c7cb2e10c24a5e5a3c2191fb (patch) | |
| tree | a88a2d1008b938e2494ec7735a862459c3f91d54 /dev/ci | |
| parent | 24c4c71236a6b12e9af6e8505c98e3ef1becb32a (diff) | |
Rename CHANGES to CHANGES.md.
Diffstat (limited to 'dev/ci')
| -rw-r--r-- | dev/ci/README.md | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/dev/ci/README.md b/dev/ci/README.md index 24952eb5b7..7870cbb51d 100644 --- a/dev/ci/README.md +++ b/dev/ci/README.md @@ -126,7 +126,7 @@ patch (or ask someone to prepare a patch) to fix the project: developer who merges the PR on Coq. There are plans to improve this, cf. [#6724](https://github.com/coq/coq/issues/6724). -Moreover your PR must absolutely update the [`CHANGES`](../../CHANGES) file. +Moreover your PR must absolutely update the [`CHANGES.md`](../../CHANGES.md) file. Advanced GitLab CI information ------------------------------ |