exclude benchmarks from DocsNav (#78)

Author: shravanngoswamii

.github/workflows/DocNav.yml

@@ -32,18 +32,21 @@ 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 .
             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
+          fi