Merge remote-tracking branch 'origin/13.0' into 13.0-store #632

	name: "Push Updates to REPO-store"

	on:
	push:

	jobs:
	repo2store:
	runs-on: ubuntu-latest
	if:
	"! endsWith(github.repository, '-store') && startsWith(github.repository,
	'itpp-labs/')"
	steps:
	- name: Checkout REPO
	uses: actions/checkout@v2-beta
	with:
	fetch-depth: 0
	# custom token is not needed for fetching REPO,
	# but the action makes some magic with authentication headers
	# which are used on pushing to REPO-store
	token: ${{ secrets.DINAR_TOKEN }}
	- name: Fetch REPO-store
	run: \|
	git remote add store https://x-access-token:${{ secrets.DINAR_TOKEN }}@github.com/${GITHUB_REPOSITORY}-store.git
	git fetch store
	- name: Merge and Push
	run: \|
	set -x
	git config --global user.email "[email protected]"
	git config --global user.name "Mitchell Admin"
	BRANCH=${GITHUB_REF##*/}
	REF=$(git rev-parse HEAD)
	git checkout -b $BRANCH-store store/$BRANCH
	git merge origin/$BRANCH $REF
	git push store $BRANCH-store:$BRANCH

Provide feedback