# HG changeset patch
# User wenzelm
# Date 1243715858 -7200
# Node ID 7015fee8c3e8d724a480bfb5ad00133d8f5d6e02
# Parent  a74ee84288a0a6dd00ff091bef8716ca94baf8e1
ISABELLE_USEDIR_OPTIONS: proper word splitting of quoted options (via array variable and special expansion, cf. "$@");

diff -r a74ee84288a0 -r 7015fee8c3e8 lib/Tools/usedir
--- 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))