fix removing repos

This commit is contained in:
Jörg Thalheim 2020-05-15 17:33:48 +01:00
parent 4178c02f17
commit 2d8183d8d0
No known key found for this signature in database
GPG key ID: 003F2096411B5F92

View file

@ -101,10 +101,11 @@ def update_combined_repo(
def remove_repo(repo: Repo, path: Path) -> None:
repo_path = path.joinpath("repos", repo.name)
repo_path = path.joinpath("repos", repo.name).resolve()
if repo_path.exists():
shutil.rmtree(repo_path)
commit_files([str(repo_path)], f"{repo.name}: remove")
with chdir(path):
commit_files([str(repo_path)], f"{repo.name}: remove")
def update_manifest(repos: List[Repo], path: Path) -> None: