String filename = "";
String filename = filenamePrefix;
  public String headerFilename() {    String filename = "";    int index = filenamePrefix.lastIndexOf('/');    if (index != -1) {      filename = filenamePrefix.substring(index);    }    return filename+".headerFile";  }