From ce5dd69f7accad2c311aa9c88dbe066d297172d0 Mon Sep 17 00:00:00 2001
From: Shravan Goswami <123811742+shravanngoswamii@users.noreply.github.com>
Date: Tue, 6 Aug 2024 23:13:08 +0530
Subject: [PATCH] exclude benchmarks from DocsNav (#78)

---
 .github/workflows/DocNav.yml | 15 +++++++++------
 1 file changed, 9 insertions(+), 6 deletions(-)

diff --git a/.github/workflows/DocNav.yml b/.github/workflows/DocNav.yml
index 14614d1f..2332710e 100644
--- a/.github/workflows/DocNav.yml
+++ b/.github/workflows/DocNav.yml
@@ -32,13 +32,16 @@ jobs:
 
           # 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
-         
+          
+          # Define file & folder to exclude (comma-separated list), Un-Comment the below line for excluding anything!
+          EXCLUDE_PATHS="benchmarks"
+          
+          # Update all HTML files in the current directory (gh-pages root), use `--exclude` only if requred!
+          ./insert_navbar.sh . $NAVBAR_URL --exclude "$EXCLUDE_PATHS"
+          
           # Remove the insert_navbar.sh file
           rm insert_navbar.sh
-         
+          
           # Check if there are any changes
           if [[ -n $(git status -s) ]]; then
             git add .
@@ -46,4 +49,4 @@ jobs:
             git push "https://${GITHUB_ACTOR}:${GITHUB_TOKEN}@github.com/${GITHUB_REPOSITORY}.git" gh-pages
           else
             echo "No changes to commit"
-          fi
+          fi
\ No newline at end of file