docs(jiminy-corpus-001): E6/E7 — full-suite green + CLAUDE.md/CHANGEL… #817
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: Auto PR from Dev Branch | |
| on: | |
| push: | |
| branches: ['**_dev*'] | |
| permissions: | |
| contents: read | |
| pull-requests: write | |
| jobs: | |
| create-pr: | |
| name: Create or Update PR | |
| runs-on: ubuntu-latest | |
| steps: | |
| - name: Checkout code | |
| uses: actions/checkout@v6 | |
| with: | |
| fetch-depth: 0 | |
| - name: Check for existing PR | |
| id: check | |
| env: | |
| GH_TOKEN: ${{ secrets.GITHUB_TOKEN }} | |
| run: | | |
| PR_URL=$(gh pr list --head "${{ github.ref_name }}" --base main --state open --json url --jq '.[0].url // empty') | |
| if [ -n "$PR_URL" ]; then | |
| echo "exists=true" >> "$GITHUB_OUTPUT" | |
| echo "url=$PR_URL" >> "$GITHUB_OUTPUT" | |
| echo "PR already exists: $PR_URL" | |
| else | |
| echo "exists=false" >> "$GITHUB_OUTPUT" | |
| echo "No open PR found, will create one" | |
| fi | |
| # A push whose content is identical to main (e.g. a manual post-merge | |
| # base-sync — see sync-dev-after-merge.yml) must not open an empty PR | |
| # (failure mode: PR #420). The automated sync pushes with GITHUB_TOKEN | |
| # and never triggers this workflow; this guard covers manual pushes. | |
| - name: Skip when branch content matches main | |
| if: steps.check.outputs.exists == 'false' | |
| id: diff | |
| run: | | |
| if git diff --quiet origin/main HEAD; then | |
| echo "empty=true" >> "$GITHUB_OUTPUT" | |
| echo "Branch content is identical to main (sync-only push) — skipping PR creation." | |
| else | |
| echo "empty=false" >> "$GITHUB_OUTPUT" | |
| fi | |
| - name: Build PR body from commits | |
| if: steps.check.outputs.exists == 'false' && steps.diff.outputs.empty == 'false' | |
| id: body | |
| run: | | |
| COMMIT_LOG=$(git log origin/main..HEAD --pretty=format:"- %s" 2>/dev/null || echo "- Initial dev branch push") | |
| { | |
| echo "body<<PREOF" | |
| echo "## Summary" | |
| echo "" | |
| echo "Development branch changes from \`${{ github.ref_name }}\`." | |
| echo "" | |
| echo "### Commits" | |
| echo "$COMMIT_LOG" | |
| echo "" | |
| echo "---" | |
| echo "*Auto-generated PR from ${{ github.ref_name }} push*" | |
| echo "PREOF" | |
| } >> "$GITHUB_OUTPUT" | |
| - name: Create PR | |
| if: steps.check.outputs.exists == 'false' && steps.diff.outputs.empty == 'false' | |
| env: | |
| GH_TOKEN: ${{ secrets.GITHUB_TOKEN }} | |
| PR_BODY: ${{ steps.body.outputs.body }} | |
| run: | | |
| gh pr create \ | |
| --head "${{ github.ref_name }}" \ | |
| --base main \ | |
| --title "dev: ${{ github.ref_name }} -> main" \ | |
| --body "$PR_BODY" |