Skip to content

Commit ce00d76

Browse files
shravanngoswamiiyebaigithub-actions[bot]
authored
New workflow for adding navigation bar (#141)
* Update make.jl for adding Navigation bar * Update docs/make.jl Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com> * added navigations bar workflow * updated workflow --------- Co-authored-by: Hong Ge <3279477+yebai@users.noreply.github.com> Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
1 parent 2a77f53 commit ce00d76

File tree

1 file changed

+48
-0
lines changed

1 file changed

+48
-0
lines changed

.github/workflows/DocsNav.yml

Lines changed: 48 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,48 @@
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

0 commit comments

Comments
 (0)