diff options
| -rwxr-xr-x | bin/clean-github-pr.py | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/bin/clean-github-pr.py b/bin/clean-github-pr.py index 68aebdcc..e914230f 100755 --- a/bin/clean-github-pr.py +++ b/bin/clean-github-pr.py @@ -82,6 +82,9 @@ def main(): os.chdir(user_work_dir) shutil.rmtree(work_area) + # make sure the branch has been pushed + time.sleep(5) + # set clean repository settings r.edit(fork, has_wiki=False, |