diff options
| -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 |