+
+# SERVER PORT
+#
+# Port to which the server is bound. The default is 10000. If the port is specified as
+# a command line parameter, the value specified on command line overides this value.
+#
+# You must RESTART the server to change the port (reload does not affect the port).
+
+port = 10000;
+