equal
deleted
inserted
replaced
104 echo "The current values are:" |
104 echo "The current values are:" |
105 echo |
105 echo |
106 echo " ML_SYSTEM=$ML_SYSTEM" |
106 echo " ML_SYSTEM=$ML_SYSTEM" |
107 echo " ML_HOME=$ML_HOME" |
107 echo " ML_HOME=$ML_HOME" |
108 echo " ML_OPTIONS=$ML_OPTIONS" |
108 echo " ML_OPTIONS=$ML_OPTIONS" |
|
109 echo " ML_PLATFORM=$ML_PLATFORM" |
109 echo |
110 echo |
110 echo " ISABELLE_USEDIR_OPTIONS=$ISABELLE_USEDIR_OPTIONS" |
111 echo " ISABELLE_USEDIR_OPTIONS=$ISABELLE_USEDIR_OPTIONS" |
111 fi |
112 fi |
112 |
113 |
113 |
114 |
152 |
153 |
153 |
154 |
154 # build it |
155 # build it |
155 |
156 |
156 SECONDS=0 |
157 SECONDS=0 |
157 echo -n "Started at "; date |
158 DATE=$(date) |
|
159 HOST=$(hostname) |
|
160 echo "Started at $DATE ($HOST)" |
158 |
161 |
159 export THIS_IS_ISABELLE_BUILD=true |
162 export THIS_IS_ISABELLE_BUILD=true |
160 |
163 |
161 for L in $MAKE_LOGICS |
164 for L in $MAKE_LOGICS |
162 do |
165 do |