src/Pure/General/json_api.scala
changeset 79044 8cc1ae43e12e
parent 78592 fdfe9b91d96e
child 79510 d8330439823a
--- a/src/Pure/General/json_api.scala	Thu Nov 23 11:36:38 2023 +0100
+++ b/src/Pure/General/json_api.scala	Thu Nov 23 11:40:49 2023 +0100
@@ -19,7 +19,7 @@
     override def toString: String = url.toString
 
     def get(route: String): HTTP.Content =
-      HTTP.Client.get(if (route.isEmpty) url else new URL(url, route))
+      HTTP.Client.get(Url.resolve(url, route))
 
     def get_root(route: String = ""): Root =
       Root(get(if_proper(route, "/" + route)).json)