This reverts commit a44bcb4746
which is not
necessary any more since the fixes to file name conversions in the previous
commit.
This reverts commit a44bcb4746
which is not
necessary any more since the fixes to file name conversions in the previous
commit.