craftui/HOW.restart_if_changed

#! /bin/sh

# developer tool to restart server when file source changes

export PATH="$(pwd)/../../../../out.gfch100_defconfig/host/usr/bin:$PATH"

pid1=
pid2=

restart() {
  [ -n "$pid1" ] && kill $pid1
  [ -n "$pid2" ] && kill $pid2
  echo "######################################################################"
  echo "# starting craftui"
  gpylint *.py
  make test
  ./craftui &
  pid1=$!
  ./craftui -2 &
  pid2=$!
  touch .started
}

onExit() {
  [ -n "$pid1" ] && kill $pid1
  [ -n "$pid2" ] && kill $pid2
  exit 1
}

trap onExit 1 2 3
restart

while sleep 1; do
  if ! kill -0 $pid1 || ! kill -0 $pid2; then
    restart
    continue
  fi
  f=$(find . -name '*.swp' -prune -o -type f -newer .started -print)
  if [ -n "$f" ]; then
    restart
    continue
  fi
done