website: deploy website from GitHub Actions (#3237)

Deploying GitHub Pages from the gh-pages branch is a classic way.
We can use actions/deploy-pages action to deploy GitHub Pages.

.github/workflows/website.yml

@@ -6,17 +6,16 @@ on:
     paths:
       - 'docs/**'
 concurrency: website
-permissions:
-  contents: write
 
 jobs:
-  website:
+  build:
     runs-on: ubuntu-latest
+    defaults:
+      run:
+        working-directory: docs
     steps:
       - name: Checkout code
         uses: actions/checkout@v4
-        with:
-          fetch-depth: 0
       - name: Setup Python
         uses: actions/setup-python@v5
         with:
@@ -26,15 +25,23 @@ jobs:
         run: pip install pipenv
       - name: Install dependencies
         run: pipenv sync
-        working-directory: docs
+      - name: Build website
-      - name: Update website
+        run: pipenv run python3 build_website.py
-        run: scripts/update-website
+      - name: Upload pages artifact
-      - name: Commit changes
+        uses: actions/upload-pages-artifact@v3
-        run: |
+        with:
-          if ! git diff --quiet; then
+          path: docs/output/
-            git add --all
+
-            git config user.name 'github-actions[bot]'
+  deploy:
-            git config user.email 'github-actions[bot]@users.noreply.github.com'
+    needs: build
-            git commit -m 'Update website'
+    permissions:
-            git push origin gh-pages
+      pages: write
-          fi
+      id-token: write
+    environment:
+      name: github-pages
+      url: ${{ steps.deployment.outputs.page_url }}
+    runs-on: ubuntu-latest
+    steps:
+      - name: Deploy to GitHub Pages
+        uses: actions/deploy-pages@v4
+        id: deployment

scripts/update-website

@@ -1,30 +0,0 @@
-#!/bin/bash
-
-# This script builds the website from the docs directory of
-# the current branch and copies it over to the gh-pages
-# branch.
-
-set -eux
-shopt -s dotglob
-
-# build website
-scriptdir=$(dirname "$0")
-cd "$scriptdir"/../docs
-rm -rf output
-mkdir output
-pipenv run python3 build_website.py
-cd ..
-
-# copy to /tmp
-tmpdir=$(mktemp -d -t jq.website.XXXXXXXXXX)
-cp -r docs/output/* "$tmpdir"
-cp .gitignore "$tmpdir"
-
-# copy to gh-pages
-git checkout gh-pages
-cp -r "$tmpdir"/* .
-cp "$tmpdir"/.gitignore .
-
-# clean up
-rm -rf "$tmpdir"
-echo SUCCESS