github: rename jj-docs-bot to jj-docs[bot]

Perhaps this will stop Github from showing jj-docs-bot as a very active
contributor in https://github.com/martinvonz/jj/pulse. This would
probably fair, even though jj-docs-bot tries its best to be a good and
helpful bot.

Regardless, this seems to be the standard on Github which has
`dependabot[bot]` and `github-actions[bot]`.

.github/workflows/docs.yml

@@ -27,8 +27,8 @@ jobs:
           poetry-version: latest
       - name: Install dependencies, compile and deploy docs
         run: |
-          git config user.name jj-docs-bot
-          git config user.email jj-docs-[email protected]
+          git config user.name jj-docs[bot]
+          git config user.email jj-docs[bot]@users.noreply.github.io
           .github/scripts/docs-build-deploy 'https://martinvonz.github.io/jj' prerelease main --push
       - name: "Show `git diff --stat`"
         run: git diff --stat gh-pages^ gh-pages || echo "(No diffs)"

.github/workflows/release.yml

@@ -123,8 +123,8 @@ jobs:
           poetry-version: latest
       - name: Install dependencies, compile and deploy docs to the "latest release" section of the website
         run: |
-          git config user.name jj-docs-bot
-          git config user.email jj-docs-[email protected]
+          git config user.name jj-docs[bot]
+          git config user.email jj-docs[bot]@users.noreply.github.io
           # Using the 'latest' tag below makes the website default
           # to this version.
           .github/scripts/docs-build-deploy 'https://martinvonz.github.io/jj' "${{ github.event.release.tag_name }}" latest --update-aliases --push