Git-subrepo: git subrepo deinit/rm/delete/remove ?

[mwithheld]

How do I remove a subrepo that's already pushed to the parent?

Should there be a
git subrepo deinit/rm/delete/remove
command?

[grimmySwe]

@mwithheld The only thing that connects the subrepo with the parent is the .gitrepo file in the subrepo. And it's you that decide when you sync it, so if you want to get rid of the entire directory, just remove it in the parent repo, if you just want to disconnect it, remove the .gitrepo file.

[mwithheld]

Super - thanks!

[varac]

Well, removing the subrepo directory is not everything you need to do - since subrepo configures a git remote and you need to remove this as well.
I'd love if complete removal could be covered by a dedicated command.