# HG changeset patch
# User wenzelm
# Date 1368809455 -7200
# Node ID 10bc73197a570fa16e1e1dc189390600117ca93e
# Parent  eaf17514aabd9a39e344d0318b1aba81bb669e18
more precise "eval", cf. isabelle build;

diff -r eaf17514aabd -r 10bc73197a57 lib/Tools/options
--- a/lib/Tools/options	Fri May 17 18:39:49 2013 +0200
+++ b/lib/Tools/options	Fri May 17 18:50:55 2013 +0200
@@ -34,7 +34,7 @@
 
 ## process command line
 
-eval "declare -a BUILD_OPTIONS=()"
+declare -a BUILD_OPTIONS=()
 LIST_OPTIONS="false"
 EXPORT_FILE=""
 
@@ -42,7 +42,7 @@
 do
   case "$OPT" in
     b)
-      BUILD_OPTIONS=($ISABELLE_BUILD_OPTIONS)
+      eval "BUILD_OPTIONS=($ISABELLE_BUILD_OPTIONS)"
       ;;
     l)
       LIST_OPTIONS="true"