Mention the correct default port.

The public server runs on port 9000, but this seems to be the default for custom servers too.

docs/api.json

@@ -29,7 +29,7 @@
           {
             "name": "port",
             "type": "number",
-            "description": "Server port. Defaults to <code>80</code>."
+            "description": "Server port. Defaults to <code>9000</code>."
           },
           {
             "name": "path",