--- a/src/Pure/Tools/flarum.scala Tue Dec 21 19:31:30 2021 +0100
+++ b/src/Pure/Tools/flarum.scala Tue Dec 21 19:42:20 2021 +0100
@@ -13,7 +13,7 @@
object Flarum
{
// see RFC3339 in https://www.php.net/manual/en/class.datetimeinterface.php
- val Date_Format = Date.Format("uuuu-MM-dd'T'HH:mm:ssxxx")
+ val Date_Format: Date.Format = Date.Format("uuuu-MM-dd'T'HH:mm:ssxxx")
def server(url: URL): Server = new Server(url)
@@ -27,6 +27,6 @@
def get_api(route: String = ""): JSON_API.Root =
JSON_API.Root(get("api" + (if (route.isEmpty) "" else "/" + route)).json)
- val api: JSON_API.Root = get_api()
+ val root: JSON_API.Root = get_api()
}
}