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 isabelle isabelle-process isabelle-interface |
77 for NAME in isabelle isabelle-process |
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" |