.github: protect .git worktree or dir

Signed-off-by: Joachim Wiberg <[email protected]>

Author: troglobit

.github/workflows/docs.yml

@@ -3,7 +3,7 @@ name: Dotty the Documenteer
 on:
   push:
     branches:
-      - master
+      - doc
     paths:
       - 'doc/**'
       - 'README.md'
@@ -51,7 +51,7 @@ jobs:
           path: site/
 
   deploy:
-    if: github.ref == 'refs/heads/master' && github.event_name == 'push'
+    if: github.ref == 'refs/heads/doc' && github.event_name == 'push'
     needs: build
     runs-on: ubuntu-latest
 
@@ -78,7 +78,9 @@ jobs:
 
       - name: Sync site to pages repo
         run: |
-          rsync -a --delete --exclude .git site/ pages/
+          rsync -a --delete --filter='P .git' --filter='P .git/**' site/ pages/
+          ls -l pages/.git
+          git -C pages status
 
       - name: Commit and push
         run: |