ISABELLE_USEDIR_OPTIONS: proper word splitting of quoted options (via array variable and special expansion, cf. "$@");

--- a/lib/Tools/usedir	Sat May 30 15:53:19 2009 +0200
+++ b/lib/Tools/usedir	Sat May 30 22:37:38 2009 +0200
@@ -175,7 +175,8 @@
   done
 }
 
-getoptions $ISABELLE_USEDIR_OPTIONS
+eval "OPTIONS=($ISABELLE_USEDIR_OPTIONS)"
+getoptions "${OPTIONS[@]}"
 
 getoptions "$@"
 shift $(($OPTIND - 1))