#!/bin/csh
# Assumes this is run from same directory where userver started.
# Normally this would point to something like /var/appropriatedir
# but we often have many people running the userver at the same time.
# kill -INT `cat userver.pid`

pkill -INT userver
set mystatus=$status
# echo "mystatus = $mystatus"
exit($mystatus)
