Skip to content

Commit 64b59b8

Browse files
Update DocsNav.yml
1 parent c9d6d16 commit 64b59b8

File tree

1 file changed

+22
-32
lines changed

1 file changed

+22
-32
lines changed

.github/workflows/DocsNav.yml

Lines changed: 22 additions & 32 deletions
Original file line numberDiff line numberDiff line change
@@ -1,49 +1,39 @@
1-
name: Add Navbar
1+
name: Rebuild docs with newest navbar
22

33
on:
4-
page_build: # Triggers the workflow on push events to gh-pages branch
5-
workflow_dispatch: # Allows manual triggering
4+
# 3:25 AM UTC every Sunday -- choose an uncommon time to avoid
5+
# periods of heavy GitHub Actions usage
66
schedule:
7-
- cron: '0 0 * * 0' # Runs every week on Sunday at midnight (UTC)
7+
- cron: '25 3 * * 0'
8+
# Whenever needed
9+
workflow_dispatch:
10+
11+
permissions:
12+
contents: write
813

914
jobs:
10-
add-navbar:
15+
update-navbar:
1116
runs-on: ubuntu-latest
12-
permissions:
13-
contents: write
17+
1418
steps:
15-
- name: Checkout gh-pages
19+
- name: Checkout gh-pages branch
1620
uses: actions/checkout@v4
1721
with:
1822
ref: gh-pages
19-
fetch-depth: 0
2023

21-
- name: Download insert_navbar.sh
22-
run: |
23-
curl -O https://raw.githubusercontent.com/TuringLang/turinglang.github.io/main/assets/scripts/insert_navbar.sh
24-
chmod +x insert_navbar.sh
24+
- name: Insert navbar
25+
uses: TuringLang/actions/DocsNav@main
26+
with:
27+
doc-path: '.'
2528

26-
- name: Update Navbar
27-
env:
28-
GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
29+
- name: Commit and push changes
2930
run: |
30-
git config user.name github-actions[bot]
31-
git config user.email github-actions[bot]@users.noreply.github.com
32-
33-
# Define the URL of the navbar to be used
34-
NAVBAR_URL="https://raw.githubusercontent.com/TuringLang/turinglang.github.io/main/assets/scripts/TuringNavbar.html"
35-
36-
# Update all HTML files in the current directory (gh-pages root)
37-
./insert_navbar.sh . $NAVBAR_URL
38-
39-
# Remove the insert_navbar.sh file
40-
rm insert_navbar.sh
41-
42-
# Check if there are any changes
4331
if [[ -n $(git status -s) ]]; then
44-
git add .
45-
git commit -m "Added navbar and removed insert_navbar.sh"
46-
git push "https://${GITHUB_ACTOR}:${GITHUB_TOKEN}@github.com/${GITHUB_REPOSITORY}.git" gh-pages
32+
git config user.name github-actions[bot]
33+
git config user.email github-actions[bot]@users.noreply.github.com
34+
git add -A
35+
git commit -m "Update navbar (automated)"
36+
git push
4737
else
4838
echo "No changes to commit"
4939
fi

0 commit comments

Comments
 (0)