equal
deleted
inserted
replaced
11 |
11 |
12 function show_settings() |
12 function show_settings() |
13 { |
13 { |
14 local PREFIX="$1" |
14 local PREFIX="$1" |
15 echo "${PREFIX}ISABELLE_BUILD_OPTIONS=\"$ISABELLE_BUILD_OPTIONS\"" |
15 echo "${PREFIX}ISABELLE_BUILD_OPTIONS=\"$ISABELLE_BUILD_OPTIONS\"" |
|
16 echo |
|
17 echo "${PREFIX}ISABELLE_BUILD_JAVA_OPTIONS=\"$ISABELLE_BUILD_JAVA_OPTIONS\"" |
16 echo |
18 echo |
17 echo "${PREFIX}ML_PLATFORM=\"$ML_PLATFORM\"" |
19 echo "${PREFIX}ML_PLATFORM=\"$ML_PLATFORM\"" |
18 echo "${PREFIX}ML_HOME=\"$ML_HOME\"" |
20 echo "${PREFIX}ML_HOME=\"$ML_HOME\"" |
19 echo "${PREFIX}ML_SYSTEM=\"$ML_SYSTEM\"" |
21 echo "${PREFIX}ML_SYSTEM=\"$ML_SYSTEM\"" |
20 echo "${PREFIX}ML_OPTIONS=\"$ML_OPTIONS\"" |
22 echo "${PREFIX}ML_OPTIONS=\"$ML_OPTIONS\"" |