Korrektur

[Christoph Gärtner]

Kleine Korrektur:

  
void checkAndSetExtension(File file, String ext, boolean ignoreCase)  
    throws FileNotFoundException, IOException  
    // Rückgabewert nicht erforderlich, da kein neues File-Objekt erzeugt wird  
{  
    if(!file.isFile())  
        throw new FileNotFoundException();  
    String name = file.getName();  
    if(ignoreCase)  
    {  
        ext = ext.toLowerCase();  
        name = name.toLowerCase();  
    }  
    if(name.endsWith("." + ext))  
        return;  
    int i = name.lastIndexOf('.');  
    if(!file.renameTo(new File(file.getParentFile(), i < 0 ?  
        name + "." + ext :  
        name.substring(0, i + 1) + ext)))  
    {  
        throw new IOException("Failed to rename " + name);  
    }  
}