Merge branch 'dev/master' #15

	name: Manpage Website Deployment
	on:
	push:
	branches:
	- master
	jobs:
	build:
	name: Manpage Generate and Deployment
	runs-on: ubuntu-20.04
	steps:
	- uses: actions/checkout@v4
	- name: Install Pre-requisites
	run: \|
	sudo apt-get update -qq
	sudo apt-get install -qq groff
	- name: Convert manpages
	run: bash -c "for x in docs/; do groff \$x -mandoc -Thtml > \${x%.}.html; done"
	- name: deploy manpages to website
	env:
	GH_TOKEN: ${{ secrets.GITLAB_DEPLOY_KEY }}
	run: \|
	git config --global user.email "[email protected]"
	git config --global user.name "Jinming Wu, Patrick"
	git clone --depth 1 https://patrick:[email protected]/wslu/website website
	bash -x extras/scripts/manpage_deploy.bash
	git --git-dir=./website/.git --work-tree=./website add -A
	git --git-dir=./website/.git --work-tree=./website commit -m "Manpage update"
	git --git-dir=./website/.git --work-tree=./website push

Provide feedback