Merge devel into master #1157

	name: Merge devel into master

	on:
	schedule:
	- cron: '0 0 * * *'

	# Allows you to run this workflow manually from the Actions tab
	workflow_dispatch:

	jobs:
	checkout-and-merge:
	runs-on: ubuntu-latest
	steps:
	- uses: actions/checkout@v3
	with:
	fetch-depth: 0
	token: ${{ secrets.TRIGGER_WORKFLOW }}
	- name: Merge devel into master
	run: \|
	git config user.name 'Gary Hu'
	git config user.email '[email protected]'
	git checkout master
	git merge-base HEAD origin/devel
	git merge --no-ff origin/devel
	git push

Provide feedback