Skip to content

Commit 3b3840d

Browse files
authored
Create DocsNav.yml (#628)
Added navigation bar workflow.
1 parent c9410de commit 3b3840d

File tree

1 file changed

+44
-0
lines changed

1 file changed

+44
-0
lines changed

.github/workflows/DocsNav.yml

+44
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,44 @@
1+
name: Add Navbar
2+
3+
on:
4+
page_build: # Triggers the workflow on push events to gh-pages branch
5+
workflow_dispatch: # Allows manual triggering
6+
7+
jobs:
8+
add-navbar:
9+
runs-on: ubuntu-latest
10+
permissions:
11+
contents: write
12+
steps:
13+
- name: Checkout gh-pages
14+
uses: actions/checkout@v4
15+
with:
16+
ref: gh-pages
17+
fetch-depth: 0
18+
19+
- name: Download insert_navbar.sh
20+
run: |
21+
curl -O https://raw.githubusercontent.com/TuringLang/turinglang.github.io/main/assets/scripts/insert_navbar.sh
22+
chmod +x insert_navbar.sh
23+
24+
- name: Update Navbar
25+
env:
26+
GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
27+
run: |
28+
git config user.name github-actions[bot]
29+
git config user.email github-actions[bot]@users.noreply.github.com
30+
31+
# Update all HTML files in the current directory (gh-pages root)
32+
./insert_navbar.sh .
33+
34+
# Remove the insert_navbar.sh file
35+
rm insert_navbar.sh
36+
37+
# Check if there are any changes
38+
if [[ -n $(git status -s) ]]; then
39+
git add .
40+
git commit -m "Added navbar and removed insert_navbar.sh"
41+
git push "https://${GITHUB_ACTOR}:${GITHUB_TOKEN}@github.com/${GITHUB_REPOSITORY}.git" gh-pages
42+
else
43+
echo "No changes to commit"
44+
fi

0 commit comments

Comments
 (0)