Paul Cadman 2d4be3b109 Pin mdbook to version 0.4.22 in docs build (#1670) ... * Pin mdbook to 0.4.22 mdbook homebrew version (used by the github action to install mdbook) was bumped to 0.4.23 eb69fcddba which seems to be incompatible with Ubuntu 20.04 glibc * Temporarily enable docs build on PRs * Revert "Temporarily enable docs build on PRs" This reverts commit e2cf41016c.		2022-12-15 16:56:27 +01:00
..
ISSUE_TEMPLATE	Label renaming (#275)	2022-07-12 12:34:48 +02:00
PULL_REQUEST_TEMPLATE	Add issues and PR templates (#261)	2022-07-08 15:19:07 +02:00
workflows	Pin mdbook to version 0.4.22 in docs build (#1670)	2022-12-15 16:56:27 +01:00