private static String mangle(String nm) {
	StringBuilder buf = new StringBuilder();
	for(int i = 0; i < nm.length(); i++) {
	    char c = nm.charAt(i);
	    if(c == '/')
		buf.append("_");
	    else
		buf.append(c);
	}
	return(buf.toString());
    }