L_extra=render_cells for tables, refs #2619 #27
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: Update Stable Docs | |
| on: | |
| release: | |
| types: [published] | |
| push: | |
| branches: | |
| - main | |
| permissions: | |
| contents: write | |
| jobs: | |
| update_stable_docs: | |
| runs-on: ubuntu-latest | |
| steps: | |
| - name: Checkout repository | |
| uses: actions/checkout@v5 | |
| with: | |
| fetch-depth: 0 # We need all commits to find docs/ changes | |
| - name: Set up Git user | |
| run: | | |
| git config user.name "Automated" | |
| git config user.email "[email protected]" | |
| - name: Create stable branch if it does not yet exist | |
| run: | | |
| if ! git ls-remote --heads origin stable | grep -qE '\bstable\b'; then | |
| # Make sure we have all tags locally | |
| git fetch --tags --quiet | |
| # Latest tag that is just numbers and dots (optionally prefixed with 'v') | |
| # e.g., 0.65.2 or v0.65.2 — excludes 1.0a20, 1.0-rc1, etc. | |
| LATEST_RELEASE=$( | |
| git tag -l --sort=-v:refname \ | |
| | grep -E '^v?[0-9]+(\.[0-9]+){1,3}$' \ | |
| | head -n1 | |
| ) | |
| git checkout -b stable | |
| # If there are any stable releases, copy docs/ from the most recent | |
| if [ -n "$LATEST_RELEASE" ]; then | |
| rm -rf docs/ | |
| git checkout "$LATEST_RELEASE" -- docs/ || true | |
| fi | |
| git commit -m "Populate docs/ from $LATEST_RELEASE" || echo "No changes" | |
| git push -u origin stable | |
| fi | |
| - name: Handle Release | |
| if: github.event_name == 'release' && !github.event.release.prerelease | |
| run: | | |
| git fetch --all | |
| git checkout stable | |
| git reset --hard ${GITHUB_REF#refs/tags/} | |
| git push origin stable --force | |
| - name: Handle Commit to Main | |
| if: contains(github.event.head_commit.message, '!stable-docs') | |
| run: | | |
| git fetch origin | |
| git checkout -b stable origin/stable | |
| # Get the list of modified files in docs/ from the current commit | |
| FILES=$(git diff-tree --no-commit-id --name-only -r ${{ github.sha }} -- docs/) | |
| # Check if the list of files is non-empty | |
| if [[ -n "$FILES" ]]; then | |
| # Checkout those files to the stable branch to over-write with their contents | |
| for FILE in $FILES; do | |
| git checkout ${{ github.sha }} -- $FILE | |
| done | |
| git add docs/ | |
| git commit -m "Doc changes from ${{ github.sha }}" | |
| git push origin stable | |
| else | |
| echo "No changes to docs/ in this commit." | |
| exit 0 | |
| fi |