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