diff --git a/distrib/platform_release.py b/distrib/platform_release.py index 7a0a2a9caf..07aa2b4c0a 100755 --- a/distrib/platform_release.py +++ b/distrib/platform_release.py @@ -44,7 +44,16 @@ def mkdir(n): def remkdir(n): - builder.utils.remkdir(n) + attempts = 10 + while attempts > 0: + try: + builder.utils.remkdir(n) + return + except: + pass + attempts -= 1 + time.sleep(5) + raise Exception("Failed to clear directory: " + n) def remove(n):