Pages

database: fix up length check of allocation strategy #352

	name: Pages
	on: [push, pull_request]
	jobs:
	mdbook:
	name: mdBook
	runs-on: ubuntu-22.04
	timeout-minutes: 30
	steps:
	- name: Checkout
	uses: actions/checkout@v3
	with:
	persist-credentials: false
	- name: Install Rust
	run: \|
	rm --recursive --force "${HOME}/.cargo" "${HOME}/.rustup"
	curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs \| sh -s -- -y
	. "${HOME}/.cargo/env"
	echo "RUSTC_VERSION=$(rustc --version \| grep --only-matching '[0-9]\+\.[0-9]\+\.[0-9]\+' \| head --lines=1)" >> $GITHUB_ENV
	- name: Install Graphviz
	run: \|
	sudo apt update \|\| true
	sudo apt --yes --no-install-recommends install graphviz
	- name: Cache mdBook
	id: cache
	uses: actions/cache@v3
	# Environment variables do not seem to work, use ~ instead.
	with:
	path: \|
	~/.cargo
	key: ubuntu-22.04-rustc-${{ env.RUSTC_VERSION }}-mdbook
	- name: Install mdBook
	run: \|
	# Fix for incompatability of mdbook graphviz with newest mdbook
	cargo install --locked [email protected] mdbook-graphviz
	- name: Configure Pages
	uses: actions/configure-pages@v2
	- name: Build book
	run: \|
	cd docs
	mdbook build
	- name: Upload book
	uses: actions/upload-pages-artifact@v1
	with:
	path: docs/book
	deploy:
	name: Deploy
	needs: mdbook
	runs-on: ubuntu-22.04
	timeout-minutes: 30
	if: ${{ github.ref == 'refs/heads/main' }}
	permissions:
	pages: write
	id-token: write
	environment:
	name: github-pages
	url: ${{ steps.deployment.outputs.page_url }}
	steps:
	- name: Checkout
	uses: actions/checkout@v3
	with:
	persist-credentials: false
	- name: Deploy Pages
	id: deployment
	uses: actions/deploy-pages@v1

Provide feedback