Tools/build pdfs only when needed #431

	name: Node CI

	on:
	push:
	branches:
	- main
	pull_request:

	jobs:
	build:
	runs-on: ubuntu-latest

	strategy:
	matrix:
	node-version: [18.x]

	steps:
	- uses: actions/checkout@v3
	- name: Use Node.js ${{ matrix.node-version }}
	uses: actions/setup-node@v3
	with:
	node-version: ${{ matrix.node-version }}
	cache: 'npm'
	- name: Setup pandoc
	uses: nikeee/setup-pandoc@v1
	with:
	pandoc-version: 3.1.2
	- name: Build docs
	run: \|
	npm ci
	npm run build
	git config user.name ${GITHUB_ACTOR}
	git config user.email ${PUSHER_EMAIL}
	git add docs//.html docs//.md docs//styles/
	for dir in docs/*/ # list directories in the form "docs/dirname/"
	do
	doc=${dir%/} # remove the trailing "/"
	doc=${doc##*/} # retain everything after the final "/"
	git diff-index --quiet HEAD $dir/.html $dir/styles/ \|\| npm run pdf $doc
	done
	git add docs//.pdf
	git diff-index --quiet HEAD docs/* \|\| ( git commit -m "auto-refreshed" && git push )
	env:
	PUSHER_EMAIL: ${{ github.event.pusher.email }}

Provide feedback