pantry/projects/github.com/nat/openplayground/entrypoint.sh

32 lines
519 B
Bash
Raw Normal View History

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
2023-07-21 18:56:29 +03:00
PORT=43873 #TODO find a port automatically!
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
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