Docs

Merge pull request #1716 from BHenkemans/fix/external_educational_links #372

	name: Docs

	# Only run this action when pushing to main.
	on:
	push:
	branches:
	- main

	# Cancel running jobs that have become stale through updates to the ref (e.g., pushes to a pull request).
	concurrency:
	group: ${{ github.workflow }}-${{ github.ref }}
	cancel-in-progress: true

	jobs:
	phpunit:
	name: phpDoc
	runs-on: ubuntu-latest

	steps:
	- name: Checkout
	uses: actions/checkout@v3

	- name: Install PHP
	uses: shivammathur/setup-php@v2
	with:
	php-version: '8.2'
	tools: phpdoc

	- name: Clone the target branch
	run: \|
	REMOTE_BRANCH="${REMOTE_BRANCH:-gh-pages}"
	REMOTE_REPO="https://${GITHUB_ACTOR}:${{ secrets.GITHUB_TOKEN }}@github.com/${GITHUB_REPOSITORY}.git"
	echo "Publishing to ${GITHUB_REPOSITORY} on branch ${REMOTE_BRANCH}"
	rm -rf docs/_site/
	git clone --depth=1 --branch="${REMOTE_BRANCH}" --single-branch --no-checkout "${REMOTE_REPO}" docs/_site/

	- name: Build site
	run: phpdoc

	- name: Deploy to GitHub Pages
	run: \|
	SOURCE_COMMIT="$(git log -1 --pretty="%an: %B" "$GITHUB_SHA")"
	pushd docs/_site &>/dev/null
	: > .nojekyll
	git add --all
	git diff --quiet --cached \|\| git -c user.name="github-actions[bot]" -c user.email="41898282+github-actions[bot]@users.noreply.github.com" \
	commit --quiet \
	--message "Deploy docs from ${GITHUB_SHA}" \
	--message "$SOURCE_COMMIT" \
	--message "Co-authored-by: ${GITHUB_ACTOR} <${GITHUB_ACTOR}@users.noreply.github.com>"
	git push
	popd &>/dev/null

Provide feedback