try to fix openplayground entrypoint

This commit is contained in:
Max Howell 2023-07-21 09:37:47 -04:00
parent e26eda10d9
commit bdb5e0d435
No known key found for this signature in database
GPG key ID: 741BB84EF5BB9EEC

View file

@ -1,12 +1,12 @@
#!/bin/bash
set -ex
set -em
source <(tea --magic=bash)
# source <(tea +curl.se)
PORT=5432 #TODO find a port!
"$d"/bin/openplayground run --port $PORT &
openplayground run --port $PORT &
PID=$!
@ -21,7 +21,9 @@ done
# open the URL once the HEAD request succeeds
if test -n "$TEA_GUI"; then
echo "{\"xyz.tea\":{\"gui\":\"http://127.0.0.1:$PORT\"}}" >&2
echo
echo '{"xyz.tea":{"gui":"http://127.0.0.1:5432"}}'
echo
else
open "http://127.0.0.1:$PORT"
fi