From d6ffbf4f3c4f9f78cb757739ea3a6cdf9635b4a3 Mon Sep 17 00:00:00 2001 From: Kovid Goyal Date: Sat, 16 Jul 2022 10:18:05 +0530 Subject: [PATCH] Rebuild before and after publishing if a branch change was needed Sometimes branches break things --- publish.py | 2 ++ 1 file changed, 2 insertions(+) diff --git a/publish.py b/publish.py index 4075491dd..e36381294 100755 --- a/publish.py +++ b/publish.py @@ -450,11 +450,13 @@ def change_to_git_master() -> Generator[None, None, None]: branch_before = current_branch() if branch_before != 'master': subprocess.check_call(['git', 'switch', 'master']) + subprocess.check_call(['make', 'debug']) try: yield finally: if branch_before != 'master': subprocess.check_call(['git', 'switch', branch_before]) + subprocess.check_call(['make', 'debug']) finally: if stash_ref_before != safe_read('.git/refs/stash'): subprocess.check_call(['git', 'stash', 'pop'])