src/Pure/mk
changeset 16376 65e2df6d8e10
parent 16131 e1b85512d87d
child 18321 3414557c2dda
equal deleted inserted replaced
16375:de1ab9e8ed4f 16376:65e2df6d8e10
    88   echo "Building $ITEM ..."
    88   echo "Building $ITEM ..."
    89   LOG="$LOGDIR/$ITEM"
    89   LOG="$LOGDIR/$ITEM"
    90 
    90 
    91   "$ISABELLE" $COPY \
    91   "$ISABELLE" $COPY \
    92     -e "val ml_system = \"$ML_SYSTEM\";" \
    92     -e "val ml_system = \"$ML_SYSTEM\";" \
       
    93     -e "val ml_platform = \"$ML_PLATFORM\";" \
    93     -e "(use\"$COMPAT\"; use\"ROOT.ML\") handle _ => exit 1;" \
    94     -e "(use\"$COMPAT\"; use\"ROOT.ML\") handle _ => exit 1;" \
    94     -f -c -q -w RAW_ML_SYSTEM Pure > "$LOG" 2>&1
    95     -f -c -q -w RAW_ML_SYSTEM Pure > "$LOG" 2>&1
    95   RC="$?"
    96   RC="$?"
    96 else
    97 else
    97   ITEM="RAW"
    98   ITEM="RAW"
    98   echo "Building $ITEM ..."
    99   echo "Building $ITEM ..."
    99   LOG="$LOGDIR/$ITEM"
   100   LOG="$LOGDIR/$ITEM"
   100 
   101 
   101   "$ISABELLE" $COPY \
   102   "$ISABELLE" $COPY \
   102     -e "val ml_system = \"$ML_SYSTEM\";" \
   103     -e "val ml_system = \"$ML_SYSTEM\";" \
       
   104     -e "val ml_platform = \"$ML_PLATFORM\";" \
   103     -e "use\"$COMPAT\" handle _ => exit 1;" \
   105     -e "use\"$COMPAT\" handle _ => exit 1;" \
   104     -q -w RAW_ML_SYSTEM RAW > "$LOG" 2>&1
   106     -q -w RAW_ML_SYSTEM RAW > "$LOG" 2>&1
   105   RC="$?"
   107   RC="$?"
   106 fi
   108 fi
   107 
   109