# HG changeset patch
# User wenzelm
# Date 1640112140 -3600
# Node ID bb0858cc574eb6c5f0608175af5982b2e8262eb9
# Parent  f03ece7155d66f56578d05cd769192202e2cc5e4
tuned signature;

diff -r f03ece7155d6 -r bb0858cc574e src/Pure/Tools/flarum.scala
--- 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()
   }
 }