2023-07-20 20:31:10 +03:00
|
|
|
#!/bin/bash
|
|
|
|
|
|
2023-07-21 16:37:47 +03:00
|
|
|
set -em
|
2023-07-20 20:31:10 +03:00
|
|
|
|
2023-08-02 18:33:56 +03:00
|
|
|
PORT=$(tea get-port)
|
2023-07-20 20:31:10 +03:00
|
|
|
|
2023-07-21 16:37:47 +03:00
|
|
|
openplayground run --port $PORT &
|
2023-07-20 20:31:10 +03:00
|
|
|
|
|
|
|
|
PID=$!
|
|
|
|
|
|
|
|
|
|
# poll until a HEAD request succeeds
|
|
|
|
|
while ! curl -Is http://127.0.0.1:$PORT | grep -q "HTTP/1.1 200 OK"; do
|
|
|
|
|
if ! kill -0 $PID; then
|
|
|
|
|
echo "webui process died!"
|
|
|
|
|
exit 1
|
|
|
|
|
fi
|
|
|
|
|
sleep 1
|
|
|
|
|
done
|
|
|
|
|
|
|
|
|
|
# open the URL once the HEAD request succeeds
|
|
|
|
|
if test -n "$TEA_GUI"; then
|
2023-07-21 16:37:47 +03:00
|
|
|
echo
|
2023-07-21 19:26:24 +03:00
|
|
|
echo "{\"xyz.tea\":{\"gui\":\"http://127.0.0.1:$PORT\"}}"
|
2023-07-21 16:37:47 +03:00
|
|
|
echo
|
2023-07-20 20:31:10 +03:00
|
|
|
else
|
|
|
|
|
open "http://127.0.0.1:$PORT"
|
|
|
|
|
fi
|
|
|
|
|
|
|
|
|
|
fg
|
