lol, i have apparently used python too much...

diff --git a/doc/protocol.txt b/doc/protocol.txt
index a9706f839f9795b1631bcf2dbc6c4423c8a949a1..da2d3394f9c03698eda199682aafb856a2f3a7b4 100644 (file)
--- a/doc/protocol.txt
+++ b/doc/protocol.txt
@@ -48,6 +48,7 @@ Initialization:
 # host: ip of server (use gethostbyname(hostname) to get from a dns name)
 # port: port of server
 function check_if_minetestserver_up($host, $port)
+{
        $socket = socket_create(AF_INET, SOCK_DGRAM, SOL_UDP);
        $timeout = array("sec" => 1, "usec" => 0);
        socket_set_option($socket, SOL_SOCKET, SO_RCVTIMEO, $timeout);
@@ -67,4 +68,5 @@ function check_if_minetestserver_up($host, $port)
                return true;
        }
        return false;
+}