From 082a85e5d0517ba48df8df7867faa53e33806278 Mon Sep 17 00:00:00 2001 From: Martin Othamar Date: Sun, 25 Oct 2026 13:43:20 +0000 Subject: [PATCH] docs: say that moving main-digdir marks the sync pull request merged A synchronization lands by moving main-digdir to the sync branch, never through the pull request's merge button, which would replay the rebuilt queue onto the old main-digdir. GitHub then marks the pull request as merged by itself, so it must not be closed or merged by hand. --- MAINTAINING-digdir.md | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/MAINTAINING-digdir.md b/MAINTAINING-digdir.md index e5e8891..6d8c7f8 100644 --- a/MAINTAINING-digdir.md +++ b/MAINTAINING-digdir.md @@ -42,7 +42,9 @@ Do this before the Microsandbox synchronization, because its submodule pins the changes](CONTRIBUTING-digdir.md#checking-kernel-configuration-changes)). 5. Disable workflow files that upstream added (see [Upstream workflows](#upstream-workflows)). 6. After approval, make sure every commit a published runtime still uses is tagged, then move the branch with - `git push --force-with-lease=main-digdir: origin sync/libkrunfw-X.Y.Z:main-digdir`. + `git push --force-with-lease=main-digdir: origin sync/libkrunfw-X.Y.Z:main-digdir`. Never use the sync + pull request's merge button, which would replay the rebuilt queue onto the old `main-digdir`. Once `main-digdir` + points at the sync branch's head, GitHub marks the pull request as merged by itself. Don't close or merge it. ## Tags and corresponding source