diff options
author | Erich Eckner <git@eckner.net> | 2019-08-29 10:41:30 +0200 |
---|---|---|
committer | Erich Eckner <git@eckner.net> | 2019-08-29 10:41:30 +0200 |
commit | a97364bc3d2045f3a485f0ec920e39315a3f7cab (patch) | |
tree | 23c13311f5011294d855bea26c806c4f8d94f13d | |
parent | 4744a472cf6b810ee3f674eb5a401caa1e17782d (diff) | |
download | builder-a97364bc3d2045f3a485f0ec920e39315a3f7cab.tar.xz |
bin/nit-picker: `git fetch` before complaining about a HEAD not being ahead of some commit
-rwxr-xr-x | bin/nit-picker | 13 |
1 files changed, 8 insertions, 5 deletions
diff --git a/bin/nit-picker b/bin/nit-picker index 562f239..9395ef4 100755 --- a/bin/nit-picker +++ b/bin/nit-picker @@ -191,11 +191,14 @@ while pgrep -x ii >/dev/null \ | mysql_run_query ) if ! git -C "${git_dir}" merge-base --is-ancestor "${git_rev}" "${current_git_head}" 2> /dev/null; then - printf 'commit %s is not an ancestor of HEAD %s in repository %s\n' \ - "${git_rev}" \ - "${current_git_head}" \ - "${git_repo}" \ - | irc_say + git -C "${git_dir}" fetch --all -p >/dev/null 2>&1 + if ! git -C "${git_dir}" merge-base --is-ancestor "${git_rev}" "${current_git_head}" 2> /dev/null; then + printf 'commit %s is not an ancestor of HEAD %s in repository %s\n' \ + "${git_rev}" \ + "${current_git_head}" \ + "${git_repo}" \ + | irc_say + fi fi fi ;; |