Skip to content

Commit

Permalink
Create DocNav.yml
Browse files Browse the repository at this point in the history
  • Loading branch information
yebai authored Jul 14, 2024
1 parent aee02e8 commit 1741416
Showing 1 changed file with 49 additions and 0 deletions.
49 changes: 49 additions & 0 deletions .github/workflows/DocNav.yml
Original file line number Diff line number Diff line change
@@ -0,0 +1,49 @@
name: Add Navbar

on:
page_build: # Triggers the workflow on push events to gh-pages branch
workflow_dispatch: # Allows manual triggering
schedule:
- cron: '0 0 * * 0' # Runs every week on Sunday at midnight (UTC)

jobs:
add-navbar:
runs-on: ubuntu-latest
permissions:
contents: write
steps:
- name: Checkout gh-pages
uses: actions/checkout@v4
with:
ref: gh-pages
fetch-depth: 0

- name: Download insert_navbar.sh
run: |
curl -O https://raw.githubusercontent.com/TuringLang/turinglang.github.io/main/assets/scripts/insert_navbar.sh
chmod +x insert_navbar.sh
- name: Update Navbar
env:
GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
run: |
git config user.name github-actions[bot]
git config user.email github-actions[bot]@users.noreply.github.com
# Define the URL of the navbar to be used
NAVBAR_URL="https://raw.githubusercontent.com/TuringLang/turinglang.github.io/main/assets/scripts/TuringNavbar.html"
# Update all HTML files in the current directory (gh-pages root)
./insert_navbar.sh . $NAVBAR_URL
# Remove the insert_navbar.sh file
rm insert_navbar.sh
# Check if there are any changes
if [[ -n $(git status -s) ]]; then
git add .
git commit -m "Added navbar and removed insert_navbar.sh"
git push "https://${GITHUB_ACTOR}:${GITHUB_TOKEN}@github.com/${GITHUB_REPOSITORY}.git" gh-pages
else
echo "No changes to commit"
fi

0 comments on commit 1741416

Please sign in to comment.