aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorAníbal Limón <anibal.limon@linaro.org>2018-04-19 16:05:03 -0500
committerAníbal Limón <anibal.limon@linaro.org>2018-04-20 09:28:13 -0500
commit59bbd42e0a6cfd17fcf570d2d4c6c78305ed52c7 (patch)
treecf5bd7d99ed4dcee9fba31631a8131e21ca3a7a8
parentcb97377b1be30ce82a165abc13cd07de8e1fc613 (diff)
ci-merge: Don't try to make manual merge if no DISPLAY
If DISPLAY isn't set (user intervention), don't try to make a conflict resolution and abort merge. Signed-off-by: Aníbal Limón <anibal.limon@linaro.org> Acked-by: Daniel Lezcano <daniel.lezcano@linaro.org> Acked-by: Amit Kucheria <amit.kucheria@linaro.org>
-rwxr-xr-xci-merge11
1 files changed, 8 insertions, 3 deletions
diff --git a/ci-merge b/ci-merge
index cc37b3b..369b57a 100755
--- a/ci-merge
+++ b/ci-merge
@@ -529,9 +529,14 @@ while read LINE; do
git merge --no-ff --no-edit $REMOTE_NAME/$REMOTE_BRANCH
if [ $? -ne 0 ]; then
- echo "Merge failed, manual merge"
- terminal -e "git mergetool -y"
- git commit -a --no-edit
+ if [ -z $DISPLAY ]; then
+ echo "Merge failed, $REMOTE_NAME $REMOTE_URL $REMOTE_BRANCH"
+ git merge --abort
+ else
+ echo "Merge failed, manual merge"
+ terminal -e "git mergetool -y"
+ git commit -a --no-edit
+ fi
fi
MERGED=$((MERGED+1))