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)