From 8d401251b833ffb6487cd1c349f3ec54942897b4 Mon Sep 17 00:00:00 2001 From: Eugene Zhuravlev Date: Fri, 13 Jul 2012 13:12:22 +0200 Subject: [PATCH] remove unused options --- jps/jps-builders/src/org/jetbrains/jps/api/GlobalOptions.java | 2 -- 1 file changed, 2 deletions(-) diff --git a/jps/jps-builders/src/org/jetbrains/jps/api/GlobalOptions.java b/jps/jps-builders/src/org/jetbrains/jps/api/GlobalOptions.java index aaf83f78d7bf..d8d40c04aa7e 100644 --- a/jps/jps-builders/src/org/jetbrains/jps/api/GlobalOptions.java +++ b/jps/jps-builders/src/org/jetbrains/jps/api/GlobalOptions.java @@ -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"; }