From 6f56c46a8b2383c4c7cb2e10c24a5e5a3c2191fb Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Fri, 5 Oct 2018 08:38:17 +0200
Subject: Rename CHANGES to CHANGES.md.

---
 dev/ci/README.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'dev/ci')

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
 ------------------------------
-- 
cgit v1.2.3