From ae219c035bfc64bf817cd1cbedafb75dfdb8e893 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Mon, 25 Nov 2019 13:20:56 +0100
Subject: Update README and make-changelog tool following introduction of
 changelog types.

---
 dev/tools/make-changelog.sh | 18 ++++++++++++++++--
 doc/changelog/README.md     | 22 +++++++++++++++-------
 2 files changed, 31 insertions(+), 9 deletions(-)

diff --git a/dev/tools/make-changelog.sh b/dev/tools/make-changelog.sh
index dbb60359cb..e1aed4560d 100755
--- a/dev/tools/make-changelog.sh
+++ b/dev/tools/make-changelog.sh
@@ -3,7 +3,7 @@
 printf "PR number? "
 read -r PR
 
-printf "Where? (type a prefix)\n"
+printf "Category? (type a prefix)\n"
 (cd doc/changelog && ls -d */)
 read -r where
 
@@ -11,11 +11,25 @@ where="doc/changelog/$where"
 if ! [ -d "$where" ]; then where=$(echo "$where"*); fi
 where="$where/$PR-$(git rev-parse --abbrev-ref HEAD).rst"
 
+printf "Type? (type first letter)\n"
+printf "[A]dded \t[C]hanged \t[D]eprecated \t[F]ixed \t[R]emoved\n"
+read -r type_first_letter
+
+case "$type_first_letter" in
+  [Aa]) type_full="Added";;
+  [Cc]) type_full="Changed";;
+  [Dd]) type_full="Deprecated";;
+  [Ff]) type_full="Fixed";;
+  [Rr]) type_full="Removed";;
+  *) printf "Invalid input!\n"
+     exit 1;;
+esac
+
 # shellcheck disable=SC2016
 # the ` are regular strings, this is intended
 # use %s for the leading - to avoid looking like an option (not sure
 # if necessary but doesn't hurt)
-printf '%s bla bla (`#%s <https://github.com/coq/coq/pull/%s>`_, by %s).' - "$PR" "$PR" "$(git config user.name)" > "$where"
+printf '%s **%s:**\n  Bla bla\n  (`#%s <https://github.com/coq/coq/pull/%s>`_,\n  by %s).' - "$type_full" "$PR" "$PR" "$(git config user.name)" > "$where"
 
 printf "Name of created changelog file:\n"
 printf "$where\n"
diff --git a/doc/changelog/README.md b/doc/changelog/README.md
index 3e0970a656..05bf710f89 100644
--- a/doc/changelog/README.md
+++ b/doc/changelog/README.md
@@ -15,12 +15,12 @@ entry in [`dev/doc/changes.md`](../../dev/doc/changes.md).
 ## How to add an entry? ##
 
 Run `./dev/tools/make-changelog.sh`: it will ask you for your PR
-number, and to choose among the predefined categories.  Afterward,
-fill in the automatically generated entry with a short description of
-your change (which should describe any compatibility issues in
-particular).  You may also add a reference to the relevant fixed
-issue, and credit reviewers, co-authors, and anyone who helped advance
-the PR.
+number, and to choose among the predefined categories, and the
+predefined types of changes.  Afterward, fill in the automatically
+generated entry with a short description of your change (which should
+describe any compatibility issues in particular).  You may also add a
+reference to the relevant fixed issue, and credit reviewers,
+co-authors, and anyone who helped advance the PR.
 
 The format for changelog entries is the same as in the reference
 manual.  In particular, you may reference the documentation you just
@@ -31,10 +31,18 @@ manual for details.
 Here is a summary of the structure of a changelog entry:
 
 ``` rst
-- Description of the changes, with possible link to
+- **Added / Changed / Deprecated / Fixed / Removed:**
+  Description of the changes, with possible link to
   :ref:`relevant-section` of the updated documentation
   (`#PRNUM <https://github.com/coq/coq/pull/PRNUM>`_,
   [fixes `#ISSUE1 <https://github.com/coq/coq/issues/ISSUE1>`_
   [ and `#ISSUE2 <https://github.com/coq/coq/issues/ISSUE2>`_],]
   by Full Name[, with help / review of Full Name]).
 ```
+
+The first line indicates the type of change.  Available types come
+from the [Keep a Changelog
+1.0.0](https://keepachangelog.com/en/1.0.0/) specification.  We
+exclude the "Security" type for now because of the absence of a
+process for handling critical bugs (proof of False) as security
+vulnerabilities.
-- 
cgit v1.2.3