blob: f0809637aa2686fbf9dc3fe52db998c28e2c25bc (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
|
#!/bin/csh -f
#(ie run the cshell on this but don't read the .cshrc)
echo version = 1.05 of kickxdvi 2002 Nov 12
# 2002 Nov 12, 1.05: (John Collins) Simplify
# 2002 Nov 5, 1.04: (John Collins) Simplify
# 2002 Oct 21, 1.04: functional!
# origin 1999Feb15.17:23:04
echo refresh xdvi processes:
# It picks up multiple processes just fine.
set whoami = `whoami`
set pid=`ps -f -u $whoami | grep xdvi.bin | grep -v grep | cut -c10-14`
if ( "$pid" != "" ) then
echo pid: $pid
/usr/bin/kill -s USR1 $pid
else
echo No xdvi.bin processes
endif
|