Skip to content

Port codegened arrow serialization to arrow1 (#8208) #2

Port codegened arrow serialization to arrow1 (#8208)

Port codegened arrow serialization to arrow1 (#8208) #2

Workflow file for this run

name: Docs deploy
on:
push:
branches: [main]
permissions:
contents: "read"
id-token: "write"
defaults:
run:
shell: bash
# The lack of `concurrency` is intentional.
# We want this job to run on every commit, even if multiple are merged in a row.
jobs:
has-label:
name: Check for PR label
runs-on: ubuntu-latest
outputs:
result: ${{ steps.find-pr.outputs.result }}
steps:
- uses: actions/checkout@v3
with:
# ref - not set, because we want to end up on the merge commit
fetch-depth: 0 # don't perform a shallow clone
# Find the PR by the number in the merge commit subject line
- name: Find PR
id: find-pr
env:
GH_TOKEN: ${{ secrets.RERUN_BOT_TOKEN }}
run: |
commit_message=$(git log --pretty=format:%s -n 1 ${{ github.sha }})
pr_number=$(echo $commit_message | grep -oP '(?<=#)\d+')
result=$(gh pr view $pr_number --json labels | jq -r 'any(.labels[].name; . == "deploy docs")')
echo "result=$result" >> $GITHUB_OUTPUT
cherry-pick:
name: Cherry-pick to docs-latest
needs: [has-label]
if: needs.has-label.outputs.result == 'true'
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v3
with:
fetch-depth: 0
token: ${{ secrets.RERUN_BOT_TOKEN }}
- name: Cherry-pick
run: |
# Setup git user
git config --global user.name "rerun-bot"
git config --global user.email "[email protected]"
# Cherry-pick the commit
git checkout docs-latest
git cherry-pick ${{ github.sha }}
git push origin docs-latest