| changeset 61131 | 83459eb76fe3 |
| parent 60106 | e0d1d9203275 |
| child 61135 | 8f7d802b7a71 |
--- a/lib/Tools/build Sun Sep 06 22:14:52 2015 +0200 +++ b/lib/Tools/build Tue Sep 08 11:44:15 2015 +0200 @@ -14,6 +14,8 @@ local PREFIX="$1" echo "${PREFIX}ISABELLE_BUILD_OPTIONS=\"$ISABELLE_BUILD_OPTIONS\"" echo + echo "${PREFIX}ISABELLE_BUILD_JAVA_OPTIONS=\"$ISABELLE_BUILD_JAVA_OPTIONS\"" + echo echo "${PREFIX}ML_PLATFORM=\"$ML_PLATFORM\"" echo "${PREFIX}ML_HOME=\"$ML_HOME\"" echo "${PREFIX}ML_SYSTEM=\"$ML_SYSTEM\""