Fix shell script error when all changed files are in .github/

- Add '|| true' to grep command to prevent exit code 1 when no matches
- Add check for non-empty filtered file list before pattern matching
- Ensures clean skip of documentation deployment for .github/ only changes

Author: AronT-TLV

.github/workflows/CI.yml

@@ -63,10 +63,10 @@ jobs:
             echo "Changed files: $CHANGED_FILES"
             
             # Filter out .github/ directory files and check for documentation-related changes
-            DOC_CHANGED_FILES=$(echo "$CHANGED_FILES" | grep -v '^\.github/')
+            DOC_CHANGED_FILES=$(echo "$CHANGED_FILES" | grep -v '^\.github/' || true)
             echo "Non-.github files: $DOC_CHANGED_FILES"
             
-            if echo "$DOC_CHANGED_FILES" | grep -qE '(^src/|^docs/|\.md$|Project\.toml$|Manifest\.toml$)'; then
+            if [ -n "$DOC_CHANGED_FILES" ] && echo "$DOC_CHANGED_FILES" | grep -qE '(^src/|^docs/|\.md$|Project\.toml$|Manifest\.toml$)'; then
               echo "Documentation-related files changed - deploying docs"
               echo "docs_changed=true" >> $GITHUB_OUTPUT
             else