diff options
author | Glenn Morris <rgm@gnu.org> | 2017-06-07 13:41:46 -0400 |
---|---|---|
committer | Glenn Morris <rgm@gnu.org> | 2017-06-07 13:41:46 -0400 |
commit | b1103a2c4f36038cbb30caba6a199744acc9e0d9 (patch) | |
tree | e7005653cc3ab7a58143ee840ae9f5b26fe2589c /make-dist | |
parent | ed226a5b34602bc476d5039fbc2e815b377d420f (diff) | |
download | emacs-b1103a2c4f36038cbb30caba6a199744acc9e0d9.tar.gz |
* make-dist: Check a release has a ChangeLog with a release notice.
Diffstat (limited to 'make-dist')
-rwxr-xr-x | make-dist | 15 |
1 files changed, 15 insertions, 0 deletions
diff --git a/make-dist b/make-dist index 0e012071640..1b4eae3e7db 100755 --- a/make-dist +++ b/make-dist @@ -297,6 +297,21 @@ if [ $check = yes ]; then make --question info || error=yes fi + ## Is this a release? + case $version in + [1-9][0-9].[0-9]) + if [ -e ChangeLog ]; then + if ! grep -q "Version $version released" ChangeLog; then + echo "No release notice in ChangeLog" + error=yes + fi + else + echo "A release must have a ChangeLog" + error=yes + fi + ;; + esac + if [ $error = yes ]; then echo "Failed checks" >&2 exit 1 |