docs: Minor improvements (#1882) #80

	name: Deploy docs
	# This job builds and deploys documentation to github pages.
	# It runs on every push to main with a change in the docs folder.
	on:
	workflow_dispatch:
	push:
	branches:
	- main
	# - "release/**"
	paths:
	- "docs/**"
	# - "x/*/.md"
	- .github/workflows/deploy-docs.yml

	permissions:
	contents: read

	jobs:
	build-and-deploy:
	permissions:
	contents: write # for JamesIves/github-pages-deploy-action to push changes in repo
	runs-on: ubuntu-latest
	steps:
	- name: Checkout 🛎️
	uses: actions/checkout@v4
	with:
	persist-credentials: false
	fetch-depth: 0
	path: "."

	- name: Setup Node.js 🔧
	uses: actions/setup-node@v4
	with:
	node-version: "21.x"

	# npm install npm should be removed when https://github.com/npm/cli/issues/4942 is fixed
	- name: Build 🔧
	run: \|
	npm install -g [email protected]
	cd docs
	./sync_versions.sh
	./build_deploy.sh

	- name: Deploy 🚀
	uses: JamesIves/[email protected]
	with:
	branch: gh-pages
	folder: ~/output
	single-commit: true

Provide feedback