25 lines
460 B
Bash
Executable File
25 lines
460 B
Bash
Executable File
#!/bin/sh
|
|
|
|
cd "$(dirname "$0")" || exit 1
|
|
|
|
if test "$#" -ne 0; then
|
|
echo "usage: run.sh" >&2
|
|
exit 1
|
|
fi
|
|
|
|
if ! test -x ./strans; then
|
|
echo "run.sh: ./strans is not executable; run make first" >&2
|
|
exit 1
|
|
fi
|
|
if ! command -v pkill >/dev/null 2>&1; then
|
|
echo "run.sh: pkill is required" >&2
|
|
exit 1
|
|
fi
|
|
|
|
uid=$(id -u) || exit 1
|
|
pkill -TERM -u "$uid" -x strans 2>/dev/null || :
|
|
sleep 0.1
|
|
pkill -KILL -u "$uid" -x strans 2>/dev/null || :
|
|
|
|
./strans map </dev/null &
|