From 7ce1501f3e31ed6745812e7dce71078f9553a719 Mon Sep 17 00:00:00 2001
From: Stefan Haller <stefan@haller-berlin.de>
Date: Sun, 2 Nov 2025 11:36:26 +0100
Subject: [PATCH] Add a script for copying the docs and schema over for release

This needs to be run immediately before creating a release.

We could go further here and use gh to create the PR, but since I'm usually
logged in with my work account to gh, this won't help me. The git push command
prints the URL to create the PR, so it's a simple matter of command-clicking it,
which is good enough for me.
---
 scripts/update_docs_for_release.sh | 31 ++++++++++++++++++++++++++++++
 1 file changed, 31 insertions(+)
 create mode 100755 scripts/update_docs_for_release.sh

diff --git a/scripts/update_docs_for_release.sh b/scripts/update_docs_for_release.sh
new file mode 100755
index 000000000..f37e36091
--- /dev/null
+++ b/scripts/update_docs_for_release.sh
@@ -0,0 +1,31 @@
+#!/bin/sh
+
+set -euo pipefail
+
+st=$(git status --porcelain)
+if [ -n "$st" ]; then
+    echo "Working directory is not clean; aborting."
+    exit 1
+fi
+
+if diff -r -q docs docs-master > /dev/null && diff -r -q schema schema-master > /dev/null; then
+    echo "No changes to docs or schema; nothing to do."
+    exit 0
+fi
+
+branch_name=update-docs-for-release
+
+if git show-ref --verify --quiet refs/heads/"$branch_name"; then
+    echo "Branch '$branch_name' already exists; aborting."
+    exit 1
+fi
+
+git checkout -b "$branch_name" --no-track origin/master
+
+git rm -r docs schema
+cp -r docs-master docs
+cp -r schema-master schema
+git add docs schema
+git commit -m "Update docs and schema for release"
+
+git push -u origin "$branch_name"