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.