diff options
Diffstat (limited to 'base')
| -rw-r--r-- | base/daemon.sh | 2 | ||||
| -rw-r--r-- | base/init.sh | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/base/daemon.sh b/base/daemon.sh index de75186..8301b3f 100644 --- a/base/daemon.sh +++ b/base/daemon.sh @@ -17,7 +17,7 @@ # along with this program. If not, see <http://www.gnu.org/licenses/>. PID=$$ -LOCK="/var/run/judge.pid" +LOCK="$JUDGE_PREFIX/judge.pid" echo $PID >$LOCK echo "Judge daemon started ... pid=$PID" >&2 diff --git a/base/init.sh b/base/init.sh index 638080d..98d653b 100644 --- a/base/init.sh +++ b/base/init.sh @@ -30,7 +30,7 @@ fi sh $LOGGER LOG error "init started ..." # TODO seams buggy FIXME -LOCK="/var/run/judgeinit.pid" +LOCK="$JUDGE_PREFIX/judge.pid" while [ -e $LOCK ] do LOCK_PID=`cat $LOCK` |