86 if [ -n "$RAW" ]; then |
86 if [ -n "$RAW" ]; then |
87 ITEM="RAW" |
87 ITEM="RAW" |
88 echo "Building $ITEM ..." |
88 echo "Building $ITEM ..." |
89 LOG="$LOGDIR/$ITEM" |
89 LOG="$LOGDIR/$ITEM" |
90 |
90 |
91 "$ISABELLE" \ |
91 "$ISABELLE_PROCESS" \ |
92 -e "val ml_system = \"$ML_SYSTEM\";" \ |
92 -e "val ml_system = \"$ML_SYSTEM\";" \ |
93 -e "val ml_platform = \"$ML_PLATFORM\";" \ |
93 -e "val ml_platform = \"$ML_PLATFORM\";" \ |
94 -e "use\"$COMPAT\" handle _ => exit 1;" \ |
94 -e "use\"$COMPAT\" handle _ => exit 1;" \ |
95 -q -w RAW_ML_SYSTEM RAW > "$LOG" 2>&1 |
95 -q -w RAW_ML_SYSTEM RAW > "$LOG" 2>&1 |
96 RC="$?" |
96 RC="$?" |
97 elif [ -n "$RAW_SESSION" ]; then |
97 elif [ -n "$RAW_SESSION" ]; then |
98 ITEM="RAW-$(basename $(dirname "$RAW_SESSION"))" |
98 ITEM="RAW-$(basename $(dirname "$RAW_SESSION"))" |
99 echo "Running $ITEM ..." |
99 echo "Running $ITEM ..." |
100 LOG="$LOGDIR/$ITEM" |
100 LOG="$LOGDIR/$ITEM" |
101 |
101 |
102 "$ISABELLE" \ |
102 "$ISABELLE_PROCESS" \ |
103 -e "use\"$RAW_SESSION\" handle _ => exit 1;" \ |
103 -e "use\"$RAW_SESSION\" handle _ => exit 1;" \ |
104 -q RAW > "$LOG" 2>&1 |
104 -q RAW > "$LOG" 2>&1 |
105 RC="$?" |
105 RC="$?" |
106 else |
106 else |
107 ITEM="Pure" |
107 ITEM="Pure" |
108 echo "Building $ITEM ..." |
108 echo "Building $ITEM ..." |
109 LOG="$LOGDIR/$ITEM" |
109 LOG="$LOGDIR/$ITEM" |
110 |
110 |
111 "$ISABELLE" \ |
111 "$ISABELLE_PROCESS" \ |
112 -e "val ml_system = \"$ML_SYSTEM\";" \ |
112 -e "val ml_system = \"$ML_SYSTEM\";" \ |
113 -e "val ml_platform = \"$ML_PLATFORM\";" \ |
113 -e "val ml_platform = \"$ML_PLATFORM\";" \ |
114 -e "(use\"$COMPAT\"; use\"ROOT.ML\") handle _ => exit 1;" \ |
114 -e "(use\"$COMPAT\"; use\"ROOT.ML\") handle _ => exit 1;" \ |
115 -f -c -q -w RAW_ML_SYSTEM Pure > "$LOG" 2>&1 |
115 -f -c -q -w RAW_ML_SYSTEM Pure > "$LOG" 2>&1 |
116 RC="$?" |
116 RC="$?" |