This repository has been archived by the owner on Jul 16, 2024. It is now read-only.

Deploy Docs #934

	name: Deploy Docs

	on:
	workflow_run:
	workflows:
	- Build Docs
	types:
	- completed
	jobs:
	deploy:
	name: Deploy Docs
	runs-on: ubuntu-latest
	steps:
	- uses: actions/setup-python@v2
	with:
	python-version: '3.9'

	- name: Get GitHub Pages Data
	uses: actions/github-script@v3
	id: pages-data
	with:
	script: \|
	const result = await github.request('GET /repos/{owner}/{repo}/pages', {
	owner: context.repo.owner,
	repo: context.repo.repo
	})
	return result.data
	- name: Lock workflow
	uses: softprops/turnstyle@v1
	env:
	GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
	with:
	poll-interval-seconds: 10

	- name: Checkout docs branch
	uses: actions/checkout@v2
	with:
	ref: refs/heads/${{ fromJSON(steps.pages-data.outputs.result).source.branch }}

	- name: Download artifact
	uses: dawidd6/action-download-artifact@v2
	with:
	workflow: ${{ github.event.workflow_run.name }}
	run_id: ${{ github.event.workflow_run.id }}
	name: doc

	- name: Update versions
	run: \|
	pip install packaging
	python update_versions.py
	- name: Get SHA & ref
	run: \|
	echo "GITHUB_SHA_SHORT=$(echo ${{ github.event.workflow_run.head_sha }} \| cut -c 1-7)" >> $GITHUB_ENV
	echo "REF=$(cat ref.txt)" >> $GITHUB_ENV
	rm -f ref.txt
	- name: Deploy docs
	run: \|
	git config user.name "GitHub Action"
	git config user.email "[email protected]"
	git add -A
	if ! git diff-index --quiet HEAD --; then
	echo "Deploying changes"
	git status
	git commit -m "Deploy docs from ${{ github.event.workflow_run.head_branch }} @ ${{ env.GITHUB_SHA_SHORT }}"
	git push -f
	else
	echo "No changes to deploy"
	exit 0
	fi
	env:
	GITHUB_TOKEN: ${{ secrets.PAGE_TOKEN }}

Provide feedback