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-07-21 16:37:47 +03:00
|
|
|
# source <(tea +curl.se)
|
2023-07-20 20:31:10 +03:00
|
|
|
|
|
|
|
|
PORT=5432 #TODO find a port!
|
|
|
|
|
|
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
|
|
|
|
|
echo '{"xyz.tea":{"gui":"http://127.0.0.1:5432"}}'
|
|
|
|
|
echo
|
2023-07-20 20:31:10 +03:00
|
|
|
else
|
|
|
|
|
open "http://127.0.0.1:$PORT"
|
|
|
|
|
fi
|
|
|
|
|
|
|
|
|
|
fg
|
