diff options
| author | Théo Zimmermann | 2019-04-16 18:27:14 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2019-05-05 19:22:32 +0200 |
| commit | 30d6ffdd4546d56c517bef5b31a862c5454240f0 (patch) | |
| tree | 7fe923020598b54da28ad0043ef12481d1e300e8 /.github | |
| parent | 6ff10c569c1684927d4cb866a159fe6f54e55abe (diff) | |
New infrastructure for the unreleased changelog.
Move existing entries.
Diffstat (limited to '.github')
| -rw-r--r-- | .github/PULL_REQUEST_TEMPLATE.md | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/.github/PULL_REQUEST_TEMPLATE.md b/.github/PULL_REQUEST_TEMPLATE.md index 73b61ee0d9..3bd3342329 100644 --- a/.github/PULL_REQUEST_TEMPLATE.md +++ b/.github/PULL_REQUEST_TEMPLATE.md @@ -16,4 +16,4 @@ Fixes / closes #???? <!-- If this is a feature pull request / breaks compatibility: --> <!-- (Otherwise, remove these lines.) --> - [ ] Corresponding documentation was added / updated (including any warning and error messages added / removed / modified). -- [ ] Entry added in CHANGES.md. +- [ ] Entry added in the changelog (see https://github.com/coq/coq/tree/master/doc/changelog#unreleased-changelog for details). |