From 97ae05b69dbd01d3e5954dbd11a01dad6f5e0cdc Mon Sep 17 00:00:00 2001 From: Johannes Altmanninger Date: Sat, 27 Sep 2025 22:55:08 +0200 Subject: [PATCH] build_tools/release.sh: actually add new docs Not quite sure for which step this is actually needed. While at it, fix the errexit issue that caused this blunder. --- build_tools/release.sh | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) diff --git a/build_tools/release.sh b/build_tools/release.sh index 638301be0..a10476a01 100755 --- a/build_tools/release.sh +++ b/build_tools/release.sh @@ -136,7 +136,10 @@ rm -rf "$tmpdir" cd "$fish_site" make git add -u - ! git ls-files --others --exclude-standard | grep . + git add docs + if git ls-files --others --exclude-standard | grep .; then + exit 1 + fi git commit --message="$(printf %s "\ | Release $version (docs) | @@ -184,7 +187,10 @@ done cd "$fish_site" make new-release git add -u - ! git ls-files --others --exclude-standard | grep . + git add docs + if git ls-files --others --exclude-standard | grep .; then + exit 1 + fi git commit --message="$(printf %s "\ | Release $version (release list update) |