# HG changeset patch
# User wenzelm
# Date 1368385081 -7200
# Node ID 4517ceb545c13b7c94262a3266ad876f4fd4d41f
# Parent  fab4ab92e8125b27104bd4ef9deb7e23b83fc953
re-init ISABELLE_PROCESS_OPTIONS to allow nested ISABELLE_PROCESS invocations, e.g. HOL-Mutabelle-ex;

diff -r fab4ab92e812 -r 4517ceb545c1 bin/isabelle-process
--- a/bin/isabelle-process	Sun May 12 20:46:17 2013 +0200
+++ b/bin/isabelle-process	Sun May 12 20:58:01 2013 +0200
@@ -222,10 +222,8 @@
   [ -p "${FIFOS[1]}" ] || fail "Bad output fifo: ${FIFOS[1]}"
   MLTEXT="$MLTEXT; Isabelle_Process.init_fifos \"${FIFOS[0]}\" \"${FIFOS[1]}\";"
 else
-  if [ -z "$ISABELLE_PROCESS_OPTIONS" ]; then
-    ISABELLE_PROCESS_OPTIONS="$ISABELLE_TMP/options"
-    "$ISABELLE_TOOL" options -x "$ISABELLE_PROCESS_OPTIONS" || fail "Failed to retrieve options"
-  fi
+  ISABELLE_PROCESS_OPTIONS="$ISABELLE_TMP/options"
+  "$ISABELLE_TOOL" options -x "$ISABELLE_PROCESS_OPTIONS" || fail "Failed to retrieve options"
   if [ "$INPUT" != RAW_ML_SYSTEM ]; then
     MLTEXT="Options.load_default () handle _ => exit 2; $MLTEXT"
   fi