[maven-release-plugin] prepare release operator-0.3.1 #153

	name: Sync docs
	on:
	push:
	branches:
	- main

	jobs:
	sync-gh-pages-doc:
	name: Sync pages
	runs-on: ubuntu-20.04
	steps:
	- name: checkout
	uses: actions/checkout@v3
	with:
	fetch-depth: 0

	- name: Configure Git
	run: \|
	git config user.name "$GITHUB_ACTOR"
	git config user.email "[email protected]"

	- name: Update doc
	run: \|
	cp -R docs /tmp/docs
	git checkout gh-pages
	rm -rf docs
	mv /tmp/docs docs
	if [ -z "$(git status --porcelain)" ]; then
	echo "Git directory is clean, nothing changed"
	git status
	exit 0
	fi
	git add -A
	git commit -m "Update docs"
	git pull --rebase origin gh-pages
	git push origin gh-pages

Provide feedback