diff -r e31bf8ed5397 -r cd266473b81b lib/Tools/install --- a/lib/Tools/install Thu Mar 10 12:11:23 2016 +0100 +++ b/lib/Tools/install Thu Mar 10 12:11:50 2016 +0100 @@ -63,7 +63,7 @@ mkdir -p "$BINDIR" || fail "Bad directory: \"$BINDIR\"" -for NAME in isabelle isabelle_process isabelle_scala_script +for NAME in isabelle isabelle_scala_script do BIN="$BINDIR/$NAME" DIST="$DISTDIR/bin/$NAME"