Add a GitHub Actions workflow to build and update website (#2603)

.github/workflows/website.yml

@@ -0,0 +1,40 @@
+name: Update website
+on:
+  push:
+    branches:
+      - master
+    paths:
+      - 'docs/**'
+concurrency: website
+permissions:
+  contents: write
+
+jobs:
+  website:
+    runs-on: ubuntu-latest
+    steps:
+      - name: Checkout code
+        uses: actions/checkout@v3
+        with:
+          fetch-depth: 0
+      - name: Setup Python
+        uses: actions/setup-python@v4
+        with:
+          python-version: '3.10'
+          cache: pipenv
+      - name: Install pipenv
+        run: pip install pipenv
+      - name: Install dependencies
+        run: pipenv sync
+        working-directory: docs
+      - name: Update website
+        run: scripts/update-website
+      - name: Commit changes
+        run: |
+          if git diff --quiet; then
+            git add --all
+            git config user.name 'github-actions[bot]'
+            git config user.email 'github-actions[bot]@users.noreply.github.com'
+            git commit -m 'Update website'
+            git push origin gh-pages
+          fi

.gitignore

@@ -47,6 +47,9 @@ m4/ltversion.m4
 m4/lt~obsolete.m4
 tests/*.trs
 
+# Docs output
+docs/output
+
 cscope.in.out
 cscope.out
 cscope.po.out

docs/.gitignore

@@ -1,3 +0,0 @@
-.DS_Store
-.sass-cache
-output/*

scripts/update-website

@@ -1,16 +1,17 @@
-#!/bin/sh
+#!/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 -eu
+set -eux
-set -o xtrace
+shopt -s dotglob
 
 # build website
-scriptdir=`dirname "$0"`
+scriptdir=$(dirname "$0")
 cd "$scriptdir"/../docs
 rm -rf output
+mkdir output
 pipenv run python3 build_website.py
 cd ..