removed function "isabelle-process", keeping "isabelle" only -- functions within the process environment might get passed through a genuine /bin/sh, which does not allow non-identifiers here;
authorwenzelm
Mon Jan 04 22:35:32 2010 +0100 (2010-01-04)
changeset 34257b5176fd9ab3c
parent 34256 da6573639ca1
child 34258 e936d3c35ce0
removed function "isabelle-process", keeping "isabelle" only -- functions within the process environment might get passed through a genuine /bin/sh, which does not allow non-identifiers here;
lib/scripts/getsettings
     1.1 --- a/lib/scripts/getsettings	Mon Jan 04 22:19:14 2010 +0100
     1.2 +++ b/lib/scripts/getsettings	Mon Jan 04 22:35:32 2010 +0100
     1.3 @@ -22,11 +22,6 @@
     1.4  ISABELLE_PROCESS="$ISABELLE_HOME/bin/isabelle-process"
     1.5  ISABELLE_TOOL="$ISABELLE_HOME/bin/isabelle"
     1.6  
     1.7 -function isabelle-process ()
     1.8 -{
     1.9 -  "$ISABELLE_PROCESS" "$@"
    1.10 -}
    1.11 -
    1.12  function isabelle ()
    1.13  {
    1.14    "$ISABELLE_TOOL" "$@"