Patch: java.io.File

[Michael Koch]

Hi list,


I just comited the attached patch from Guilhem Lavaux which was in our 
BTS for a long time already.


Michael


09-20-03 Guilhem Lavaux <address@hidden>

         * java/io/File.java:
        (File(File,String)): fixed the behaviour according to JDK 1.4.1.
        dirPath should not be initialized to the full path if directory
        is null, but to "/" if directory.getPath() is "" and the full path
        in the other cases. A null name should throw a NullPointerException.

file.diff
Description: Text Data