Docs

Lock file maintenance #495

	name: Docs

	on: [push, pull_request]

	jobs:
	build:
	runs-on: ubuntu-latest

	steps:
	- uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4

	- name: generate documentation
	run: cargo doc --no-deps

	- name: generate book
	run: \|
	cargo install mdbook
	cd book/text
	mdbook build

	- name: prep deployment branch
	if: github.ref == 'refs/heads/main'
	run: \|
	mkdir -p dist
	cp -r target/doc/* dist/
	cp -r book/text/book dist/
	cd dist
	git init
	git add -A
	git config --local user.email "action@github.com"
	git config --local user.name "GitHub Action"
	git commit -m 'deploy'

	- name: push deployment branch
	uses: ad-m/github-push-action@d91a481090679876dfc4178fef17f286781251df # v0.8.0
	if: github.ref == 'refs/heads/main'
	with:
	github_token: ${{ secrets.GITHUB_TOKEN }}
	branch: gh-pages
	force: true
	directory: ./dist

Provide feedback