equal
deleted
inserted
replaced
61 |
61 |
62 echo "referring to distribution at \"$DISTDIR\"" |
62 echo "referring to distribution at \"$DISTDIR\"" |
63 |
63 |
64 mkdir -p "$BINDIR" || fail "Bad directory: \"$BINDIR\"" |
64 mkdir -p "$BINDIR" || fail "Bad directory: \"$BINDIR\"" |
65 |
65 |
66 for NAME in isabelle isabelle_scala_script |
66 for NAME in isabelle isabelle_java isabelle_scala_script |
67 do |
67 do |
68 BIN="$BINDIR/$NAME" |
68 BIN="$BINDIR/$NAME" |
69 DIST="$DISTDIR/bin/$NAME" |
69 DIST="$DISTDIR/bin/$NAME" |
70 echo "installing $BIN" |
70 echo "installing $BIN" |
71 rm -f "$BIN" |
71 rm -f "$BIN" |
72 echo "#!/usr/bin/env bash" > "$BIN" || fail "Cannot write file: $BIN" |
72 echo "#!/usr/bin/env bash" > "$BIN" || fail "Cannot write file: $BIN" |
73 echo >> "$BIN" |
73 echo >> "$BIN" |
74 echo "exec \"$DIST\" \"\$@\"" >> "$BIN" |
74 echo "exec \"$DIST\" \"\$@\"" >> "$BIN" |
75 chmod +x "$BIN" |
75 chmod +x "$BIN" |
76 done |
76 done |
77 |
|