Rev 9379 | Go to most recent revision | Show entire file | Regard whitespace | Details | Blame | Last modification | View Log | RSS feed
Rev 9379 | Rev 9393 | ||
---|---|---|---|
Line 3... | Line 3... | ||
3 | import sys |
3 | import sys |
4 | import shutil |
4 | import shutil |
Line 5... | Line 5... | ||
5 | 5 | ||
Line 6... | Line -... | ||
6 | import workspace.build |
- | |
7 | - | ||
8 | if len(sys.argv) < 2 or sys.argv[1] != "--remove-everything": |
- | |
9 | print(f"Please call `{sys.argv[0]} --remove-everything` if you really want to remove all your workspace files") |
- | |
10 | exit() |
6 | import workspace.build |
11 | 7 | ||
Line 12... | Line 8... | ||
12 | # Remove workspace folder |
8 | # Remove workspace folder |
13 | shutil.rmtree("workspace", ignore_errors = True) |
9 | shutil.rmtree("workspace", ignore_errors = True) |