File tree Expand file tree Collapse file tree 1 file changed +48
-0
lines changed
.github/workflows/.github/workflows Expand file tree Collapse file tree 1 file changed +48
-0
lines changed Original file line number Diff line number Diff line change 1+ name : Add Navbar
2+
3+ on :
4+ workflow_run :
5+ workflows : ["Documentation"] # add workflow names that generates docs in this list like `workflows: ["Docs Workflow", "Previews Workflow]`
6+ types :
7+ - completed
8+ workflow_dispatch : # Allows manual triggering
9+
10+ jobs :
11+ add-navbar :
12+ runs-on : ubuntu-latest
13+ if : ${{ github.event.workflow_run.conclusion == 'success' }}
14+ permissions :
15+ contents : write
16+ steps :
17+ - name : Checkout gh-pages
18+ uses : actions/checkout@v4
19+ with :
20+ ref : gh-pages
21+ fetch-depth : 0
22+
23+ - name : Download insert_navbar.sh
24+ run : |
25+ curl -O https://raw.githubusercontent.com/TuringLang/turinglang.github.io/main/assets/scripts/insert_navbar.sh
26+ chmod +x insert_navbar.sh
27+
28+ - name : Update Navbar
29+ env :
30+ GITHUB_TOKEN : ${{ secrets.GITHUB_TOKEN }}
31+ run : |
32+ git config user.name github-actions[bot]
33+ git config user.email github-actions[bot]@users.noreply.github.com
34+
35+ # Update all HTML files in the current directory (gh-pages root)
36+ ./insert_navbar.sh .
37+
38+ # Remove the insert_navbar.sh file
39+ rm insert_navbar.sh
40+
41+ # Check if there are any changes
42+ if [[ -n $(git status -s) ]]; then
43+ git add .
44+ git commit -m "Added navbar and removed insert_navbar.sh"
45+ git push "https://${GITHUB_ACTOR}:${GITHUB_TOKEN}@github.com/${GITHUB_REPOSITORY}.git" gh-pages
46+ else
47+ echo "No changes to commit"
48+ fi
You can’t perform that action at this time.
0 commit comments