From 30d6ffdd4546d56c517bef5b31a862c5454240f0 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Tue, 16 Apr 2019 18:27:14 +0200
Subject: New infrastructure for the unreleased changelog.

Move existing entries.
---
 dev/doc/MERGING.md | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'dev/doc')

diff --git a/dev/doc/MERGING.md b/dev/doc/MERGING.md
index 3f1b470878..c9eceb1270 100644
--- a/dev/doc/MERGING.md
+++ b/dev/doc/MERGING.md
@@ -71,8 +71,9 @@ those external projects should have been prepared (cf. the relevant sub-section
 in the [CI README](../ci/README.md#Breaking-changes) and the PR can be tested
 with these fixes thanks to ["overlays"](../ci/user-overlays/README.md).
 
-Moreover the PR must absolutely update the [`CHANGES.md`](../../CHANGES.md) or
-the [`dev/doc/changes.md`](changes.md) file.
+Moreover the PR author *must* add an entry to the [unreleased
+changelog](../../doc/changelog/README.md) or to the
+[`dev/doc/changes.md`](changes.md) file.
 
 If overlays are missing, ask the author to prepare them and label the PR with
 the [needs: overlay](https://github.com/coq/coq/labels/needs%3A%20overlay) label.
-- 
cgit v1.2.3