Merge branch 'main' of github.com:josehu07/summerset-private into min…

…or-publish
josehu07 · Jul 16, 2024 · 49aef7e · 49aef7e
2 parents 0554dfc + 898f3e7
commit 49aef7e
Showing 1 changed file with 4 additions and 1 deletion.
diff --git 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!")