chore: remove docs mirror (AztecProtocol#3122)

No longer deemed useful, extra repo was confusing

Author: ludamad

.github/workflows/mirror_repos.yml

@@ -12,31 +12,8 @@ on:
     - cron: '0 2 * * *'
 
 jobs:
-  mirror-to-docs-repo:
-    runs-on: ubuntu-latest
-    steps:
-      - name: Checkout
-        uses: actions/checkout@v3
-        with:
-          fetch-depth: 0
-          token: ${{ secrets.AZTEC_BOT_GITHUB_TOKEN }}
-      - name: Push to docs repo
-        run: |
-          SUBREPO_PATH=docs
-          git config --global user.name AztecBot
-          git config --global user.email [email protected]
-
-          if ./scripts/git_subrepo.sh push $SUBREPO_PATH --branch=main; then
-            git fetch # in case a commit came after this
-            git rebase origin/master
-            git commit --amend -m "$(git log -1 --pretty=%B) [skip ci]"
-            git push
-          fi
-
   mirror-to-build-system-repo:
     runs-on: ubuntu-latest
-    # Force sequential.
-    needs: mirror-to-docs-repo
     steps:
       - name: Checkout
         uses: actions/checkout@v3