--- 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))