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