Join GitHub today
GitHub is home to over 40 million developers working together to host and review code, manage projects, and build software together.Sign up
IIRC, the deletion does not yet check, whether there is a repository checked out. Additionally, it might not even know it, because there might one be checked out on a different computer. So maybe we check locally only, delete, if locally possible, and then add another check in the merge-process, so that we deny deletion during merge (and instead recover an entry) if it is still needed on another computer.