#!/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