diff options
Diffstat (limited to 'util')
| -rwxr-xr-x | util/kill_all (renamed from util/kill) | 0 | ||||
| -rwxr-xr-x | util/kill_session | 5 | ||||
| -rwxr-xr-x | util/run_all | 2 |
3 files changed, 6 insertions, 1 deletions
diff --git a/util/kill b/util/kill_all index e82f822..e82f822 100755 --- a/util/kill +++ b/util/kill_all diff --git a/util/kill_session b/util/kill_session new file mode 100755 index 0000000..1f57c81 --- /dev/null +++ b/util/kill_session @@ -0,0 +1,5 @@ +#!/usr/bin/zsh -x + +lsof /srv/postedit/sessions/$1/work/session.out | cut -d " " -f 2- | /srv/postedit/scripts/strips | cut -d " " -f 1 | grep -v PID | xargs kill +lsof /srv/postedit/sessions/$1/work/session.out + diff --git a/util/run_all b/util/run_all index a873e63..e82ced9 100755 --- a/util/run_all +++ b/util/run_all @@ -4,6 +4,6 @@ for i in `cat ../sessions/sessions | cut -f 1`; do echo $i ./util/run_session $i & - sleep 60 + sleep 10 done |