diff --git a/.github/workflows/DocsNav.yml b/.github/workflows/DocsNav.yml deleted file mode 100644 index 14614d1fd..000000000 --- a/.github/workflows/DocsNav.yml +++ /dev/null @@ -1,49 +0,0 @@ -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