From 898f3e7ccb2f6012d2b87d2bf4a45d5d8662f956 Mon Sep 17 00:00:00 2001 From: Guanzhou Hu Date: Mon, 15 Jul 2024 23:45:10 -0700 Subject: [PATCH] adding public repo publish script --- publish/public_repo_trim.py | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/publish/public_repo_trim.py b/publish/public_repo_trim.py index e86a6e72..1e5c0562 100644 --- a/publish/public_repo_trim.py +++ b/publish/public_repo_trim.py @@ -53,8 +53,11 @@ def num_leading_spaces(line): def remove_path(path): - if os.path.exists(path): + if os.path.isdir(path): shutil.rmtree(path) + print(f" RM {path}/") + elif os.path.isfile(path): + os.unlink(path) print(f" RM {path}") else: print(f" RM {path} NOT FOUND!")