Get the default path to the user's config file, which is used unless an alternative name has been specified via system properties or #setUserConfigFile. @return the default user config file path.
()
| 945 | * @return the default user config file path. |
| 946 | */ |
| 947 | public static String getDefaultUserConfigFileName() { |
| 948 | String filePrefix = ""; |
| 949 | if(runningOnUnix()) filePrefix = "."; |
| 950 | |
| 951 | String userConfigName = |
| 952 | System.getProperty("user.home") + Strings.getFileSep() + filePrefix |
| 953 | + GATE_DOT_XML; |
| 954 | return userConfigName; |
| 955 | } // getDefaultUserConfigFileName |
| 956 | |
| 957 | /** |
| 958 | * Get the default path to the user's session file, which is used unless an |