#!/bin/bashset-xe
cd"$(gitrev-parse--show-toplevel)"sourcetests/chutney/arti.run
kill-sINT"$pid";# wait $pid, but $pid was started by a different process
tail--pid="$pid"-f/dev/null
./chutney/chutneystop"$target"sourcetests/chutney/arti.run
exit"$result"