Update performance results (#15) #46

	name: Compile documentation (dev/pre-release)
	on:
	push:
	branches:
	- main
	workflow_dispatch: {}
	repository_dispatch:
	types: [publish-docs-dev]

	permissions:
	contents: write

	jobs:
	deploy:
	runs-on: ubuntu-latest
	steps:
	- uses: actions/checkout@v4
	with:
	path: pages
	fetch-depth: 0

	- uses: actions/checkout@v4
	with:
	repository: Jelly-RDF/jelly-protobuf
	path: proto

	- name: Generate Protobuf reference
	run: \|
	mkdir -p pages/docs/specification/proto
	cp proto/*.proto pages/docs/specification/proto
	# Remove double newlines in comments to avoid breaking markdown tables
	# See: https://github.com/pseudomuto/protoc-gen-doc/issues/274
	find proto/.proto -type f -exec perl -0777 -i -pe "s\|\n[ \t]+//[ \t]\n\|\n\|igs" {} \;
	find proto/*.proto -type f -exec perl -0777 -i -pe "s\|(https?[^\s]+)\|[\1](\1)\|igs" {} \;
	docker run --rm -v $(pwd)/proto:/protos -v $(pwd)/pages/docs/specification:/out pseudomuto/protoc-gen-doc --doc_opt=markdown,reference.md

	- uses: actions/setup-python@v5
	with:
	python-version: '3.11'
	cache: pip
	cache-dependency-path: 'pages/requirements.txt'

	- name: Install dependencies
	working-directory: ./pages
	run: pip install -r requirements.txt

	- name: Deploy site
	working-directory: ./pages
	run: \|
	export TAG='main'
	export JVM_TAG='main'
	export PROTO_PATH='../proto'
	git fetch origin gh-pages --depth=1
	git config user.name ci-bot
	git config user.email [email protected]
	mike deploy --push --alias-type=redirect --title "Development version" --update-aliases dev latest

Provide feedback