equal
deleted
inserted
replaced
72 # standalone binaries |
72 # standalone binaries |
73 |
73 |
74 if [ -n "$BINDIR" ]; then |
74 if [ -n "$BINDIR" ]; then |
75 mkdir -p "$BINDIR" || fail "Bad directory: $BINDIR" |
75 mkdir -p "$BINDIR" || fail "Bad directory: $BINDIR" |
76 |
76 |
77 for NAME in isatool isabelle-process isabelle-interface |
77 for NAME in isabelle isabelle-process isabelle-interface |
78 do |
78 do |
79 BIN="$BINDIR/$NAME" |
79 BIN="$BINDIR/$NAME" |
80 DIST="$DISTDIR/bin/$NAME" |
80 DIST="$DISTDIR/bin/$NAME" |
81 echo "installing $BIN" |
81 echo "installing $BIN" |
82 rm -f "$BIN" |
82 rm -f "$BIN" |
83 echo "#!/usr/bin/env bash" > "$BIN" || fail "Cannot write file: $BIN" |
83 echo "#!/usr/bin/env bash" > "$BIN" || fail "Cannot write file: $BIN" |
84 echo >> "$BIN" |
84 echo >> "$BIN" |
85 echo "exec \"$DIST\" \"\$@\"" >> "$BIN" |
85 echo "exec \"$DIST\" \"\$@\"" >> "$BIN" |
86 chmod +x "$BIN" |
86 chmod +x "$BIN" |
87 done |
87 done |
88 for NAME in Isabelle isabelle |
|
89 do |
|
90 BIN="$BINDIR/$NAME" |
|
91 echo "installing $BIN" |
|
92 rm -f "$BIN" |
|
93 cp "$ISABELLE_HOME/bin/$NAME" "$BIN" || fail "Cannot write file: $BIN" |
|
94 chmod +x "$BIN" |
|
95 done |
|
96 fi |
88 fi |