The disc storing the gitlab remotes has run out of space. This has caused the web GUI to become non-functional so I can’t delete a repository through the GUI. Are there any issues with deleting a remote repo through the command line? My fear is there’s additional data stored elsewhere that will cause errors with the web GUI if the repository is deleted manually.