From: Jean Privat <jean@pryen.org>
Date: Fri, 26 Aug 2016 00:20:52 +0000 (-0400)
Subject: githumerge: skip if already merged
X-Git-Url: http://nitlanguage.org

githumerge: skip if already merged

Signed-off-by: Jean Privat <jean@pryen.org>
---

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."