equal
deleted
inserted
replaced
125 return filename.toString(); |
125 return filename.toString(); |
126 } |
126 } |
127 |
127 |
128 public static String nameFromPath(Path file) throws IOException { |
128 public static String nameFromPath(Path file) throws IOException { |
129 String f = nullSafeFileName(file); |
129 String f = nullSafeFileName(file); |
130 return f.substring(0, f.length() - JFCParser.FILE_EXTENSION.length()); |
130 if (f.endsWith(JFCParser.FILE_EXTENSION)) { |
|
131 return f.substring(0, f.length() - JFCParser.FILE_EXTENSION.length()); |
|
132 } else { |
|
133 return f; |
|
134 } |
131 } |
135 } |
132 |
136 |
133 // Invoked by DCmdStart |
137 // Invoked by DCmdStart |
134 public static Configuration createKnown(String name) throws IOException, ParseException { |
138 public static Configuration createKnown(String name) throws IOException, ParseException { |
135 // Known name, no need for permission |
139 // Known name, no need for permission |