fix #1954 #546

	name: build dev manual

	on:
	push:
	paths:
	- 'manual/**'
	branches:
	- master
	tags:
	- v**
	pull_request:
	paths:
	- 'manual/**'
	branches:
	- master

	jobs:
	build_dev_manual:
	name: Build developer documentation
	runs-on: ubuntu-latest
	if: github.ref == 'refs/heads/master'
	steps:
	- uses: actions/[email protected]
	- name: Set up JDK 11
	uses: actions/setup-java@v1
	with:
	java-version: 11
	- name: Generate dev documentation website
	run: sh ./scripts/doc.sh buildDev
	- name: Commit files
	run: \|
	git config --local user.email "[email protected]"
	git config --local user.name "otoroshi-github-actions"
	git add --all
	git commit -am "Update dev documentation websites"
	- name: Push documentation
	uses: ad-m/github-push-action@master
	with:
	github_token: ${{ secrets.GITHUB_TOKEN }}

Provide feedback