Method getPrefix

output/java/1.4.17/Misc.java:127–133

(String name)

    }

    public static String getPrefix(String name) {
        if ( name==null ) return "/";
        String parent = getParent(name);
        String prefix = parent;
        if ( !parent.endsWith("/") ) prefix +='/';
        return prefix;
    }

    public static String replaceEscapes(String s) {
        s = s.replaceAll("\n", "\\\\n");