Mara Bos 8403ad2258 Make rushlink --delete work with urls that have a file extension.		2020-03-24 14:42:54 +01:00
..
rushlink	Make rushlink --delete work with urls that have a file extension.	2020-03-24 14:42:54 +01:00