.github: fix deploy issue

 - We already have the SHA
 - Use 'git add -A' to handle deleted files too

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
 
@@ -82,19 +82,18 @@ jobs:
 
       - name: Commit and push
         run: |
-          cd pages
-
+          cd pages/
           if [ -z "$(git status --porcelain)" ]; then
               exit 0
           fi
 
           SRC_REPO="${GITHUB_REPOSITORY}"
-          SRC_REF="$(git -C .. rev-parse --short HEAD)"
+          SRC_REF="${GITHUB_SHA::7}"
           SRC_URL="https://github.com/${SRC_REPO}/commit/${SRC_REF}"
 
           git config user.name "GitHub Actions"
           git config user.email "[email protected]"
-          git add .
+          git add -A
           git commit -m "docs: update from ${SRC_REPO}@${SRC_REF}" \
                      -m "For details, see ${SRC_URL}"
           git push