diff options
| author | Sean Whitton <spwhitton@spwhitton.name> | 2016-04-02 12:38:55 -0700 |
|---|---|---|
| committer | Sean Whitton <spwhitton@spwhitton.name> | 2016-04-02 12:38:55 -0700 |
| commit | 194792196508f113e203a9aef6d5d9b9f9c2b9d2 (patch) | |
| tree | 6b49993ae16ea504a2145d9db9fd2e2c37d1e3db | |
| parent | 53296aa807f5fce47eb8630cb9e61c9ea2b69870 (diff) | |
| download | dotfiles-194792196508f113e203a9aef6d5d9b9f9c2b9d2.tar.gz | |
wait for github branch push to avoid errors
| -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, |