(refs #1379)Prepend "/" if specified prefix does not start with it
1 parent 9c9876c commit 572ea5bf47365dbbe22b96360da2877884cdc5fa
@Naoki Takezoe Naoki Takezoe authored on 28 Dec 2016
Showing 1 changed file
View
3
■■
src/main/java/JettyLauncher.java
} else if(dim[0].equals("--port")) {
port = Integer.parseInt(dim[1]);
} else if(dim[0].equals("--prefix")) {
contextPath = dim[1];
if(!contextPath.startsWith("/")){
contextPath = "/" + contextPath;
}
} else if(dim[0].equals("--gitbucket.home")){
System.setProperty("gitbucket.home", dim[1]);
}
}