diff options
Diffstat (limited to 'dev/tools')
| -rwxr-xr-x | dev/tools/make-changelog.sh | 10 |
1 files changed, 7 insertions, 3 deletions
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 |