diff --git a/support/patch-update b/support/patch-update index e37cf7c9..15959613 100755 --- a/support/patch-update +++ b/support/patch-update @@ -82,6 +82,9 @@ if ($incl_generated_files) { system "rm -rf a b"; } +sleep 1 if $last_touch == time; +system "git-checkout master"; + exit;