#
# Functions for the release scripts
#
check_return_code()
{
  if [ $? != 0 ]; then
     echo " "
     echo "$1"
     echo " "
     exit 1
  fi
}