event #1257

	name: CI

	on:
	[push, workflow_dispatch, repository_dispatch]

	jobs:
	build:
	runs-on: ubuntu-latest
	if: "!contains(github.event.head_commit.message, '[skip ci]')"

	steps:
	- uses: actions/checkout@v1
	name: Checkout

	- name: Checkout tools repo
	uses: actions/checkout@v3
	with:
	repository: Gwion/GwionSite
	path: GwionSite

	- name: GwionSite tools
	run: bash GwionSite/install.sh

	- name: Dependencies
	run: bash scripts/update.sh

	- name: MdBook
	uses: peaceiris/actions-mdbook@v1
	with:
	mdbook-version: 'latest'

	- name: GIT things
	run: \|
	git config --global user.email "action@github.com"
	git config --global user.name "GitHub Action"

	- name: Checkout benchmark repo
	uses: actions/checkout@v3
	with:
	repository: Gwion/gwion-benchmark
	path: gwion-benchmark
	ref: results

	- name: Core Reference
	run: \|
	echo "# Core Reference" > docs/Reference/README.mdr
	echo "compiler generated documentation" >> docs/Reference/README.mdr
	echo '```gwion' >> docs/Reference/README.mdr
	./gwion --cdoc >> docs/Reference/README.mdr
	echo '```' >> docs/Reference/README.mdr

	- name: Plugin Reference
	run: \|
	echo README.md > docs/Reference/Plugins/list
	for plug in *.so; do bash scripts/mk_page.sh $plug; done

	- name: Build book
	run: PATH=$PWD:$PATH make build

	- name: Push book
	run: \|
	git add -f book
	git commit -m "add book"
	git remote set-url origin https://${{ secrets.GWION_TOKEN }}@github.com/Gwion/Gwion.git
	git push origin :gh-pages \|\| true
	git subtree push --prefix book origin gh-pages

Provide feedback