mirror of
https://gitflic.ru/project/openide/openide.git
synced 2026-09-27 10:03:11 +07:00
remove unused options
This commit is contained in:
@@ -8,9 +8,7 @@ public interface GlobalOptions {
|
||||
String USE_MEMORY_TEMP_CACHE_OPTION = "use.memory.temp.cache";
|
||||
String USE_EXTERNAL_JAVAC_OPTION = "use.external.javac.process";
|
||||
String HOSTNAME_OPTION = "localhost.name";
|
||||
String PING_INTERVAL_MS_OPTION = "server.ping.interval";
|
||||
String GENERATE_CLASSPATH_INDEX_OPTION = "generate.classpath.index";
|
||||
String MAX_SIMULTANEOUS_BUILDS_OPTION = "max.simultaneous.builds";
|
||||
String COMPILE_PARALLEL_OPTION = "compile.parallel";
|
||||
String COMPILE_PARALLEL_MAX_THREADS_OPTION = "compile.parallel.max.threads";
|
||||
}
|
||||
|
||||
Reference in New Issue
Block a user