diff options
| author | Alon Zakai <alonzakai@gmail.com> | 2011-11-11 16:35:48 -0800 |
|---|---|---|
| committer | Alon Zakai <alonzakai@gmail.com> | 2011-11-11 16:35:48 -0800 |
| commit | 8e0fd1cb75afb4d4843f89b889a634da171d32fe (patch) | |
| tree | a00115f067abf266d27cf2c4a47d50d82f75b329 /tools | |
| parent | cf885bc56f0661542b7486a4bd6613a5d6666a53 (diff) | |
fix for building projects when they already exist
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/shared.py | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/tools/shared.py b/tools/shared.py index 1220f98e..5cc06240 100644 --- a/tools/shared.py +++ b/tools/shared.py @@ -230,6 +230,8 @@ class Building: temp_dir = build_dir if copy_project: project_dir = os.path.join(temp_dir, name) + if os.path.exists(project_dir): + shutil.rmtree(project_dir) shutil.copytree(path_from_root('tests', name), project_dir) # Useful in debugging sometimes to comment this out else: project_dir = build_dir |