Method setFile

basex-core/src/main/java/org/basex/gui/GUIOptions.java:268–270

Sets the string value of an option. The file path will be normalized. @param option option to be set @param file file to be assigned

(final StringOption option, final IOFile file)

   * @param file file to be assigned
   */
  public synchronized void setFile(final StringOption option, final IOFile file) {
    set(option, file.normalize().path());
  }

  /**
   * Returns the supported XML suffixes.