2019-04-23 04:00:00 +02:00
|
|
|
--- a/net/minecraft/server/DedicatedServerSettings.java
|
|
|
|
+++ b/net/minecraft/server/DedicatedServerSettings.java
|
|
|
|
@@ -1,15 +1,21 @@
|
|
|
|
package net.minecraft.server;
|
|
|
|
|
|
|
|
import java.util.function.UnaryOperator;
|
|
|
|
+// CraftBukkit start
|
|
|
|
+import java.io.File;
|
|
|
|
+import joptsimple.OptionSet;
|
|
|
|
+// CraftBukkit end
|
|
|
|
|
|
|
|
public class DedicatedServerSettings {
|
|
|
|
|
|
|
|
private final java.nio.file.Path path;
|
|
|
|
private DedicatedServerProperties properties;
|
|
|
|
|
2020-08-11 23:00:00 +02:00
|
|
|
- public DedicatedServerSettings(IRegistryCustom iregistrycustom, java.nio.file.Path java_nio_file_path) {
|
2019-04-23 04:00:00 +02:00
|
|
|
- this.path = java_nio_file_path;
|
2020-08-11 23:00:00 +02:00
|
|
|
- this.properties = DedicatedServerProperties.load(iregistrycustom, java_nio_file_path);
|
2019-04-23 04:00:00 +02:00
|
|
|
+ // CraftBukkit start
|
2020-08-11 23:00:00 +02:00
|
|
|
+ public DedicatedServerSettings(IRegistryCustom iregistrycustom, OptionSet optionset) {
|
2019-04-23 04:00:00 +02:00
|
|
|
+ this.path = ((File) optionset.valueOf("config")).toPath();
|
2020-08-11 23:00:00 +02:00
|
|
|
+ this.properties = DedicatedServerProperties.load(iregistrycustom, path, optionset);
|
2019-04-23 04:00:00 +02:00
|
|
|
+ // CraftBukkit end
|
|
|
|
}
|
|
|
|
|
|
|
|
public DedicatedServerProperties getProperties() {
|