From f675224169d666d85d34ce0f0b895aa1fd3e5e64 Mon Sep 17 00:00:00 2001 From: Jean Privat Date: Thu, 25 Aug 2016 20:20:52 -0400 Subject: [PATCH] githumerge: skip if already merged Signed-off-by: Jean Privat --- contrib/github_merge.nit | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/contrib/github_merge.nit b/contrib/github_merge.nit index a1971fd..46e6105 100644 --- a/contrib/github_merge.nit +++ b/contrib/github_merge.nit @@ -122,6 +122,10 @@ for arg in args do print "Commit {sha} not in local repository; did you fetch github?" return end + if system("git merge-base --is-ancestor {sha} HEAD") == 0 then + print "Is already merged." + continue + end if system("git merge --no-ff --no-commit {sha}") != 0 then system("cp mergemsg `git rev-parse --git-dir`/MERGE_MSG") print "Problem during merge... Let's do the commit manually." -- 1.7.9.5