promote: dev → stage #23

Merged
will.anderson merged 14 commits from dev into stage 2026-05-09 23:36:00 +00:00
Showing only changes of commit 15c70f0e26 - Show all commits
+11 -1
View File
@@ -43,7 +43,17 @@ jobs:
echo "Merge commit: $COMMIT_MSG"
# Gitea merge commits: "Merge pull request '...' (#N) from dev into stage"
# Direct branch merges: "Merge branch 'dev' into stage"
if echo "$COMMIT_MSG" | grep -qE " from dev into stage$| 'dev' into stage$"; then
# tea pr merge with custom title: any subject line is possible, so
# fall back to checking git parents — if the second parent is on dev
# the merge came from dev regardless of the commit subject.
SECOND_PARENT=$(git log -1 --pretty=format:"%P" HEAD | awk '{print $2}')
FROM_DEV=""
if [ -n "$SECOND_PARENT" ]; then
if git merge-base --is-ancestor "$SECOND_PARENT" origin/dev 2>/dev/null; then
FROM_DEV=1
fi
fi
if echo "$COMMIT_MSG" | grep -qE " from dev into stage$| 'dev' into stage$" || [ -n "$FROM_DEV" ]; then
echo "Source branch check: OK (merged from dev)"
else
echo "ERROR: stage only accepts merges from dev."