#if [ -z $GEXTGNOME_DEVEL ] ; then
#  echo "GNOME Support Library environment variable GEXTGNOME_DEVEL not set."
#  echo "Ensure that this extension is installed and that you have sourced devel.bash"
#  exit -1
#fi

if [ "x$GEXTDIVA" = "x" ] ; then
  echo "Diva.js extension environment variable GEXTDIVA not set."
  echo "Have you sourced the extension's setup file, e.g. setup.bash?"
  exit -1
fi