Update docs

This commit is contained in:
github-actions
2023-05-09 19:56:30 +00:00
parent 47e38c7bda
commit 6ae39c4dc1
579 changed files with 30453 additions and 21485 deletions

View File

@ -0,0 +1,19 @@
#!/usr/bin/env bash
set -euo pipefail
DIRNAME="$(dirname -- "${BASH_SOURCE[0]}")"
PATCH="$DIRNAME/upgradeable.patch"
error() {
echo Error: "$*" >&2
exit 1
}
if ! git diff-files --quiet ":!$PATCH" || ! git diff-index --quiet HEAD ":!$PATCH"; then
error "Repository must have no staged or unstaged changes"
fi
if ! git apply -3 "$PATCH"; then
error "Fix conflicts and run $DIRNAME/patch-save.sh"
fi