This directory
https://github.com/bjoernkjoshanssen/jla/tree/main/(*%20%20Title%3A%20%20%20%20%20%20HOL/Examples
was created by accident and now it seems I am unable to delete it via the github.com interface. Any idea why?
The URL is so anomalous that I am not even able to include a link here, but you may drop the URL in the address bar.
>Solution :
I went ahead to open a PR which helps delete the accidentally created directory and moves the file that was in it to the root directory.
I hope this helps.
If you’re wondering how I did it, I cloned the repo and used VS code to delete it. I was also able to to do it using the github.dev interface.