equal
deleted
inserted
replaced
98 fi |
98 fi |
99 [ "$?" = 0 ] || exit "$?" |
99 [ "$?" = 0 ] || exit "$?" |
100 |
100 |
101 DISTBASE="$BASE_DIR/dist-${DISTNAME}" |
101 DISTBASE="$BASE_DIR/dist-${DISTNAME}" |
102 |
102 |
103 "$ISABELLE_TOOL" makedist_bundles "$DISTBASE/${DISTNAME}.tar.gz" |
103 |
|
104 for PLATFORM_FAMILY in linux macos windows |
|
105 do |
|
106 |
|
107 echo |
|
108 echo "*** $PLATFORM_FAMILY ***" |
|
109 |
|
110 "$ISABELLE_TOOL" makedist_bundle "$DISTBASE/${DISTNAME}.tar.gz" "$PLATFORM_FAMILY" |
104 [ "$?" = 0 ] || exit "$?" |
111 [ "$?" = 0 ] || exit "$?" |
|
112 |
|
113 done |
105 |
114 |
106 "$THIS/build_library" $JOBS "$DISTBASE/${DISTNAME}_${ISABELLE_PLATFORM_FAMILY}.tar.gz" |
115 "$THIS/build_library" $JOBS "$DISTBASE/${DISTNAME}_${ISABELLE_PLATFORM_FAMILY}.tar.gz" |
107 |
116 |