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, 04 Jan 2010 22:35:32 +0100
changeset 34257 b5176fd9ab3c
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
--- a/lib/scripts/getsettings	Mon Jan 04 22:19:14 2010 +0100
+++ b/lib/scripts/getsettings	Mon Jan 04 22:35:32 2010 +0100
@@ -22,11 +22,6 @@
 ISABELLE_PROCESS="$ISABELLE_HOME/bin/isabelle-process"
 ISABELLE_TOOL="$ISABELLE_HOME/bin/isabelle"
 
-function isabelle-process ()
-{
-  "$ISABELLE_PROCESS" "$@"
-}
-
 function isabelle ()
 {
   "$ISABELLE_TOOL" "$@"