From 87787ce81b52675f19b96f780de232be00ce6f77 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 12 Nov 2019 17:13:31 +0100
Subject: Printing name of change log file in changelog script.

---
 dev/tools/make-changelog.sh | 10 +++++++---
 1 file changed, 7 insertions(+), 3 deletions(-)

(limited to 'dev/tools')

diff --git a/dev/tools/make-changelog.sh b/dev/tools/make-changelog.sh
index ec59a6047f..dbb60359cb 100755
--- a/dev/tools/make-changelog.sh
+++ b/dev/tools/make-changelog.sh
@@ -1,9 +1,9 @@
 #!/bin/sh
 
-echo "PR number"
+printf "PR number? "
 read -r PR
 
-echo "Where? (type a prefix)"
+printf "Where? (type a prefix)\n"
 (cd doc/changelog && ls -d */)
 read -r where
 
@@ -17,10 +17,14 @@ where="$where/$PR-$(git rev-parse --abbrev-ref HEAD).rst"
 # 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 "Name of created changelog file:\n"
+printf "$where\n"
+
 giteditor=$(git config core.editor)
 if [ "$giteditor" ]; then
     $giteditor "$where"
 elif [ "$EDITOR" ]; then
     $EDITOR "$where"
-else echo "$where"
+else
+    printf "Describe the changes in the above file\n"
 fi
-- 
cgit v1.2.3