From b25d572fd28567c9c5ea0be575d28489b29bb6a7 Mon Sep 17 00:00:00 2001
From: Hong Ge <3279477+yebai@users.noreply.github.com>
Date: Tue, 16 Jul 2024 14:58:05 +0100
Subject: [PATCH] Create DocNav.yml

---
 .github/workflows/DocNav.yml | 49 ++++++++++++++++++++++++++++++++++++
 1 file changed, 49 insertions(+)
 create mode 100644 .github/workflows/DocNav.yml

diff --git a/.github/workflows/DocNav.yml b/.github/workflows/DocNav.yml
new file mode 100644
index 00000000..14614d1f
--- /dev/null
+++ b/.github/workflows/DocNav.yml
@@ -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