fonsp / Pluto.jl

🎈 Simple reactive notebooks for Julia
https://plutojl.org/
MIT License
4.93k stars 284 forks source link

Specify host name in ServerOptions #2729

Closed flwyd closed 9 months ago

flwyd commented 9 months ago

Pluto.Configuration.ServerOptions offers the following options which can affect the link which is shown on the console:

When I start Pluto on a remote server, I would like to show a link which uses a host name rather than an IP address. This is useful for a couple reasons:

Using root_url to accomplish this is tricky because the port isn't known in advance when using port_hint, so Pluto.run(host="0.0.0.0", root_url="http://myhost.local:1234/") risks getting the URL wrong if 1234 is already in use while Pluto.run(host="0.0.0.0", root_url="http://myhost.local:1234/", port=1234) risks failing to start.

Some possible solutions: (1) add a host_name option which is used as host_str in WebServer.pretty_address or (2) replace a token like {PORT} in root_url once the port has been selected.