#!/bin/sh
#
# This script will start jetty if it not started or its PID
# doesn't indicate that it is running.
#
# set -x

. $HOME/.jettyrc

touch $HOME/.jettystopped

$JETTY_HOME/bin/jetty.sh stop
	
#RMIPID=`ps -ae | grep rmiregistry | cut -b -5`
#kill -9 $RMIPID
