diff -r f993cbffc42a -r 0642cbb60c98 lib/Tools/install --- a/lib/Tools/install Sun Nov 30 12:58:20 2008 +0100 +++ b/lib/Tools/install Sun Nov 30 14:03:45 2008 +0100 @@ -74,7 +74,7 @@ if [ -n "$BINDIR" ]; then mkdir -p "$BINDIR" || fail "Bad directory: $BINDIR" - for NAME in isabelle isabelle-process isabelle-interface + for NAME in isabelle isabelle-process do BIN="$BINDIR/$NAME" DIST="$DISTDIR/bin/$NAME"