| #! /bin/sh |
| |
| # developer tool to restart server when file source changes |
| |
| pid= |
| |
| restart() { |
| [ -n "$pid" ] && kill $pid |
| echo "######################################################################" |
| echo "# starting craftui" |
| gpylint *.py |
| make test |
| ./craftui & |
| pid=$! |
| touch .started |
| } |
| |
| onExit() { |
| [ -n "$pid" ] && kill $pid |
| exit 1 |
| } |
| |
| trap onExit 1 2 3 |
| restart |
| |
| while sleep 1; do |
| if ! kill -0 $pid; then |
| restart |
| continue |
| fi |
| f=$(find . -name '*.swp' -prune -o -type f -newer .started -print) |
| if [ -n "$f" ]; then |
| restart |
| continue |
| fi |
| done |