Skip to content

Commit

Permalink
Merge CI checkout fix
Browse files Browse the repository at this point in the history
This merge fixes a mistake I made merging #1461. The issue was that the bot_pr_format_base.sh script tried to create the same branch twice.

Related PR: #1469
  • Loading branch information
MarcelKoch authored Nov 24, 2023
2 parents fa71990 + a3cd494 commit 5cc844f
Showing 1 changed file with 0 additions and 4 deletions.
4 changes: 0 additions & 4 deletions .github/bot-pr-format-base.sh
Original file line number Diff line number Diff line change
Expand Up @@ -9,10 +9,6 @@ git remote add fork "$HEAD_URL"
git fetch fork "$HEAD_BRANCH"
git fetch origin "$BASE_BRANCH"

# checkout current PR head
LOCAL_BRANCH=format-tmp-$HEAD_BRANCH
git checkout -b $LOCAL_BRANCH fork/$HEAD_BRANCH

git config user.email "ginkgo.library@gmail.com"
git config user.name "ginkgo-bot"

Expand Down

0 comments on commit 5cc844f

Please sign in to comment.