Get the original, initialisation-time, GATE development environment configuration data (initialised from gate.xml ).
()
| 836 | * configuration data (initialised from <TT>gate.xml</TT>). |
| 837 | */ |
| 838 | public static OptionsMap getOriginalUserConfig() { |
| 839 | return originalUserConfig; |
| 840 | } // getOriginalUserConfig |
| 841 | |
| 842 | /** |
| 843 | * Update the GATE development environment configuration data in the user's |