Michiel de Boer wrote: > Is there another way though to achieve the same thing?
You can always run wget and then rename the file afterward. If this happens often, you might want write a shell script to handle it. Of course, If you want all the references to the file to be converted, the script will be a little more complicated. :-) Tony
