jerry73204 merged NEWSLabNTU/nano-ros#3886 · November 14, 2026 18:51 ci(phase-489 W11): a push to main skips the fast tier the merge queue already ran on its commit #3886 phase-489 W11 (user-accepted, from the manager; HEADGREEN is dropped). main is rebase-merged, so the commit a push brings in is the same commit the… +341 -14