Return to the master branch at the end.

diff --git a/support/patch-update b/support/patch-update
index e37cf7c9c6a26f3df9397de08a91e7c27c0b1777..15959613bfa123c7627d17a7100051485f8e1fce 100755 (executable)
--- 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;