scripts/pull_github_pr.sh: clean up after failed cherry-pick

When pull_github_pr.sh uses git cherry-pick to merge a single-patch
pull request, this cherry-pick can fail. A typical example is trying
to merge a patch that has actually already been merged in the past,
so cherry-pick reports that the patch, after conflict resolution,
is empty.

When cherry-pick fails, it leaves the working directory in an annoying
mid-cherry-pick state, and today the user needs to manually call
"git cherry-pick --abort" to return to the normal state. The script
should it automatically - so this is what we do in this patch.

Signed-off-by: Nadav Har'El <nyh@scylladb.com>

scripts/pull_github_pr.sh

@@ -57,7 +57,11 @@ closes="${NL}${NL}Closes #${PR_NUM}${NL}"
 if [[ $nr_commits == 1 ]]; then
 	commit=$(git log --pretty=oneline HEAD..FETCH_HEAD | awk '{print $1}')
 	message="$(git log -1 "$commit" --format="format:%s%n%n%b")"
-	git cherry-pick $commit
+	if ! git cherry-pick $commit
+	then
+		git cherry-pick --abort
+		exit 1
+	fi
 	git commit --amend -m "${message}${closes}"
 else
 	git merge --no-ff --log=1000 FETCH_HEAD -m "Merge '$PR_TITLE' from $USER_NAME" -m "${PR_DESCR}${closes}"