Не могу удалить каталог github со странным именем
Этот каталог
https://github.com/bjoernkjoshanssen/jla/tree/main/(*%20%20Title%3A%20%20%20%20%20%20HOL/Examples
был создан случайно, и теперь кажется, что я не могу удалить его через интерфейс github.com. Есть идеи, почему? URL-адрес настолько аномален, что я даже не могу разместить здесь ссылку, но вы можете добавить URL-адрес в адресную строку.
Ответы 2
Я пошел дальше и открыл PR, который помогает удалить случайно созданный каталог и перемещает файл, который был в нем, в корневой каталог.
Надеюсь, это поможет.
Если вам интересно, как я это сделал, я клонировал репозиторий и использовал код VS, чтобы удалить его. Я также смог сделать это, используя интерфейс github.dev.
Вы можете сделать это самостоятельно из пользовательского интерфейса GitHub:
Странно, что у вас это не сработало — я форкнул ваш репозиторий и у меня всё заработало.
Хорошо, возможно, я использовал похожее меню в правой части экрана. Не уверен, что это имеет значение
Вот что не работает, как ни странно.