Merge pull request #1122 from LKuemmel/wiki #55

	name: Publish docs to Wiki
	# based on https://nimblehq.co/blog/create-github-wiki-pull-request
	# Trigger this action only if there are changes pushed to the docs/** directory under the main branch
	on:
	push:
	paths:
	- docs/** # This includes all sub folders
	branches:
	- master # This can be changed to any branch of your preference

	env:
	USER_TOKEN: ${{ secrets.WIKI_ACTION_TOKEN }} # This is the repository secret
	USER_NAME: LKuemmel # Enter the username of your (bot) account
	USER_EMAIL: [email protected] # Enter the e-mail of your (bot) account
	OWNER: ${{ github.event.repository.owner.name }} # This is the repository owner
	REPOSITORY_NAME: ${{ github.event.repository.name }} # This is the repository name

	jobs:
	publish_docs_to_wiki:
	name: Publish docs to Wiki
	runs-on: ubuntu-latest
	steps:
	- name: Checkout repository
	uses: actions/checkout@v3

	# 1. Create folder named `tmp_wiki`
	# 2. Initialize Git
	# 3. Pull old Wiki content
	- name: Pull content from wiki
	run: \|
	mkdir tmp_wiki
	cd tmp_wiki
	git init
	git config user.name $USER_NAME
	git config user.email $USER_EMAIL
	git pull https://[email protected]/$OWNER/$REPOSITORY_NAME.wiki.git
	# 4. Synchronize differences between `docs` & `tmp_wiki`
	# 5. Push new Wiki content
	- name: Push content to wiki
	run: \|
	rsync -av --delete docs/ tmp_wiki/ --exclude .git
	cd tmp_wiki
	git add .
	git commit -m "Update Wiki content"
	git push -f --set-upstream https://[email protected]/$OWNER/$REPOSITORY_NAME.wiki.git master

Provide feedback