diff options
| author | Glenn Morris <rgm@gnu.org> | 2018-10-25 21:57:53 -0700 |
|---|---|---|
| committer | Glenn Morris <rgm@gnu.org> | 2018-10-25 21:57:53 -0700 |
| commit | 3575dd8e8c7edaa904220e5f59240b91814b5564 (patch) | |
| tree | d3f455b3be61a77b6e1e514d014e90b933716579 /admin | |
| parent | 9dd95bf0b12c8ddba82acae741f944743e37cdd8 (diff) | |
| download | emacs-3575dd8e8c7edaa904220e5f59240b91814b5564.tar.gz | |
* admin/automerge: Abort if NEWS gets modified.
Diffstat (limited to 'admin')
| -rwxr-xr-x | admin/automerge | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/admin/automerge b/admin/automerge index e88711f8d6d..b320369d174 100755 --- a/admin/automerge +++ b/admin/automerge @@ -174,6 +174,12 @@ merge () merge +## FIXME it would be better to trap this in gitmerge. +## NEWS should never be modified, only eg NEWS.26. +git diff --stat --cached origin/master | grep -q "NEWS " && \ + die "NEWS has been modified" + + [ "$build" ] || exit 0 |