Skip to content

Rebuild docs with newest navbar #45

Rebuild docs with newest navbar

Rebuild docs with newest navbar #45

Workflow file for this run

name: Rebuild docs with newest navbar
on:
# 3:25 AM UTC every Sunday -- choose an uncommon time to avoid
# periods of heavy GitHub Actions usage
schedule:
- cron: '25 3 * * 0'
# Whenever needed
workflow_dispatch:
permissions:
contents: write
jobs:
update-navbar:
runs-on: ubuntu-latest
steps:
- name: Checkout gh-pages branch
uses: actions/checkout@v4
with:
ref: gh-pages
- name: Insert navbar
uses: TuringLang/actions/DocsNav@main
with:
doc-path: '.'
- name: Commit and push changes
run: |
if [[ -n $(git status -s) ]]; then
git config --global user.email "github-actions[bot]@users.noreply.github.com"
git config --global user.name "GitHub Actions"
git add -A
git commit -m "Update navbar (automated)"
git push
else
echo "No changes to commit"
fi