diff options
| -rw-r--r-- | src/main/java/com/google/devtools/build/lib/packages/WorkspaceFactory.java | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/src/main/java/com/google/devtools/build/lib/packages/WorkspaceFactory.java b/src/main/java/com/google/devtools/build/lib/packages/WorkspaceFactory.java index dff613b162..1982200325 100644 --- a/src/main/java/com/google/devtools/build/lib/packages/WorkspaceFactory.java +++ b/src/main/java/com/google/devtools/build/lib/packages/WorkspaceFactory.java @@ -506,8 +506,11 @@ public class WorkspaceFactory { if (workspaceDir != null) { workspaceEnv.update("__workspace_dir__", workspaceDir.getPathString()); } - File jreDirectory = new File(System.getProperty("java.home")); - workspaceEnv.update("DEFAULT_SERVER_JAVABASE", jreDirectory.getParentFile().toString()); + File javaHome = new File(System.getProperty("java.home")); + if (javaHome.getName().equalsIgnoreCase("jre")) { + javaHome = javaHome.getParentFile(); + } + workspaceEnv.update("DEFAULT_SERVER_JAVABASE", javaHome.toString()); for (EnvironmentExtension extension : environmentExtensions) { extension.updateWorkspace(workspaceEnv); |