| changeset 5393 | 7299e531d481 |
| parent 5386 | 4325d853494a |
| child 6256 | e17fb80b3ce1 |
| 5392:a98dfbb19c80 | 5393:7299e531d481 |
|---|---|
139 echo |
139 echo |
140 echo "ML_SYSTEM=$ML_SYSTEM" |
140 echo "ML_SYSTEM=$ML_SYSTEM" |
141 echo "ML_HOME=$ML_HOME" |
141 echo "ML_HOME=$ML_HOME" |
142 echo "ML_OPTIONS=$ML_OPTIONS" |
142 echo "ML_OPTIONS=$ML_OPTIONS" |
143 echo |
143 echo |
144 echo "ISABELLE_USEDIR_OPTIONS=$ISABELLE_USEDIR_OPTIONS" |
|
145 echo |
|
144 fi |
146 fi |
145 |
147 |
146 |
148 |
147 # build it |
149 # build it |
148 |
150 |