# HG changeset patch # User wenzelm # Date 857745023 -3600 # Node ID bc6d915b8019165367f2c6137a68889f2c5b6de5 # Parent e1d15eabb64d72ae928c84da620448517c25f248 renamed SYSTEM to RAW_ML_SYSTEM; diff -r e1d15eabb64d -r bc6d915b8019 bin/isabelle --- a/bin/isabelle Fri Mar 07 15:29:46 1997 +0100 +++ b/bin/isabelle Fri Mar 07 15:30:23 1997 +0100 @@ -32,7 +32,7 @@ echo " INPUT (default \"$DEFAULT_LOGIC\") and OUTPUT specify in/out heaps." echo " These are either names to be searched in the Isabelle path, or actual" echo " file names (then containing at least one /)." - echo " If INPUT is \"SYSTEM\", just start the bare bones ML system." + echo " If INPUT is \"RAW_ML_SYSTEM\", just start the bare bones ML system." echo exit 1 } @@ -117,7 +117,7 @@ [ -z "$INPUT" ] && INPUT="$DEFAULT_LOGIC" case "$INPUT" in - SYSTEM) + RAW_ML_SYSTEM) INFILE="" ;; */*) diff -r e1d15eabb64d -r bc6d915b8019 src/Pure/mk --- a/src/Pure/mk Fri Mar 07 15:29:46 1997 +0100 +++ b/src/Pure/mk Fri Mar 07 15:30:23 1997 +0100 @@ -29,6 +29,6 @@ $ISABELLE \ -e "val ml_system = \"$ML_SYSTEM\";" \ -e "use\"$COMPAT\"; use\"ROOT.ML\" handle _ => exit 1;" \ - -cq SYSTEM Pure + -cq RAW_ML_SYSTEM Pure chmod -w $ISABELLE_OUTPUT_DIR/Pure