docs: Reorganize ValidMind Library "portal" around sorted Jupyter Not… #418
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| name: Merge main into staging | |
| on: | |
| push: | |
| branches: | |
| - main | |
| permissions: | |
| contents: write | |
| id-token: write | |
| pull-requests: write | |
| jobs: | |
| merge-main-into-staging: | |
| runs-on: ubuntu-latest | |
| steps: | |
| - name: Checkout staging branch | |
| uses: actions/checkout@v3 | |
| with: | |
| ref: staging | |
| fetch-depth: 0 | |
| - name: Configure git | |
| run: | | |
| git config --global user.name "github-actions[bot]" | |
| git config --global user.email "github-actions[bot]@users.noreply.github.com" | |
| - name: Merge in main branch | |
| run: | | |
| git merge --no-ff origin/main | |
| # NEW: detect the PR that triggered this push to main (if any) | |
| - name: Determine source PR (if any) | |
| id: source-pr | |
| env: | |
| GH_TOKEN: ${{ secrets.GITHUB_TOKEN }} | |
| run: | | |
| prs=$(gh api \ | |
| repos/${{ github.repository }}/commits/${{ github.sha }}/pulls \ | |
| -H "Accept: application/vnd.github+json") | |
| number=$(echo "$prs" | jq -r '.[0].number // empty') | |
| if [ -n "$number" ]; then | |
| echo "prefix=PR#$number — " >> "$GITHUB_OUTPUT" | |
| else | |
| echo "prefix=" >> "$GITHUB_OUTPUT" | |
| fi | |
| - name: Create pull request | |
| id: pr-number | |
| uses: peter-evans/create-pull-request@v5 | |
| with: | |
| token: ${{ secrets.GITHUB_TOKEN }} | |
| branch: update-staging-${{ github.run_id }} | |
| title: '${{ steps.source-pr.outputs.prefix }}Merge main into staging' | |
| body: 'Automatically merge main into staging branch.' | |
| - name: Merge pull request (with retries) | |
| if: ${{ steps.pr-number.outputs.pull-request-number != '' }} | |
| env: | |
| GH_TOKEN: ${{ secrets.GITHUB_TOKEN }} | |
| run: | | |
| for i in {1..5}; do | |
| gh pr merge --merge --auto "${{ steps.pr-number.outputs.pull-request-number }}" && break | |
| echo "Merge failed, retrying in 10 seconds ..." | |
| sleep 10 | |
| done | |
| - name: Delete pull request branch | |
| if: ${{ success() && steps.pr-number.outputs.pull-request-number != '' }} | |
| run: gh api -X DELETE "repos/${{ github.repository }}/git/refs/heads/update-staging-${{ github.run_id }}" | |
| env: | |
| GH_TOKEN: ${{ secrets.GITHUB_TOKEN }} |