Rename CHANGES to CHANGES.md.

3 files changed, 4 insertions, 4 deletions

diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh
index 5f07aa8fca..b8bea755e0 100755
--- a/dev/build/windows/makecoq_mingw.sh
+++ b/dev/build/windows/makecoq_mingw.sh
@@ -1374,7 +1374,7 @@ function copy_coq_license {
     # FIXME: this is not the micromega license
     # It only applies to code that was copied into one single file!
     install -D README.md                      "$PREFIXCOQ/license_readme/coq/ReadMe.md"
-    install -D CHANGES                        "$PREFIXCOQ/license_readme/coq/Changes.txt"
+    install -D CHANGES.md                     "$PREFIXCOQ/license_readme/coq/Changes.md"
     install -D INSTALL                        "$PREFIXCOQ/license_readme/coq/Install.txt"
     install -D doc/README.md                  "$PREFIXCOQ/license_readme/coq/ReadMeDoc.md" || true
   fi
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
 ------------------------------
diff --git a/dev/doc/MERGING.md b/dev/doc/MERGING.md
index c0cd9c8cdd..000f21c254 100644
--- a/dev/doc/MERGING.md
+++ b/dev/doc/MERGING.md
@@ -54,7 +54,7 @@ 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`](../../CHANGES) file.
+Moreover the PR must absolutely update the [`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.
@@ -93,7 +93,7 @@ When the PR has conflicts, the assignee can either:
 
 In both cases, CI should be run again.
 
-In some rare cases (e.g. the conflicts are in the CHANGES file), it is ok to fix
+In some rare cases (e.g. the conflicts are in the `CHANGES.md` file), it is ok to fix
 the conflicts in the merge commit (following the same steps as below), and push
 to `master` directly. Don't use the GitHub interface to fix these conflicts.