Give me 5 seconds to terminate the process with Ctrl-C key

Hit Ctrl-C during the git checkout process is dangerous.
It is also dangerous to terminate during make.
This commit adds a 5s sleep time between each loop, so
you can terminate the process by Ctrl-C.

1 files changed, 3 insertions, 0 deletions

diff --git a/bibisect_build.py b/bibisect_build.py
index a16fb29..7d4b82e 100755
--- a/bibisect_build.py
+++ b/bibisect_build.py
@@ -314,5 +314,8 @@ if __name__ == "__main__":
         if push_to_bare:
             cmd = f"git -C {repr(target)} push {repr(target_bare)} master --tags"
             run_process(cmd)
+
+        print("Sleeping for 5s, type  Ctrl-C to terminate this script")
+        time.sleep(5)
     
     print("All Done!")