lib/Tools/install
changeset 28504 7ad7d7d6df47
parent 26577 50f47cc2af72
child 28650 a7ba12e0d3b7
     1.1 --- a/lib/Tools/install	Sat Oct 04 16:19:49 2008 +0200
     1.2 +++ b/lib/Tools/install	Sat Oct 04 17:40:56 2008 +0200
     1.3 @@ -74,7 +74,7 @@
     1.4  if [ -n "$BINDIR" ]; then
     1.5    mkdir -p "$BINDIR" || fail "Bad directory: $BINDIR"
     1.6  
     1.7 -  for NAME in isatool isabelle-process isabelle-interface
     1.8 +  for NAME in isabelle isabelle-process isabelle-interface
     1.9    do
    1.10      BIN="$BINDIR/$NAME"
    1.11      DIST="$DISTDIR/bin/$NAME"
    1.12 @@ -85,12 +85,4 @@
    1.13      echo "exec \"$DIST\" \"\$@\"" >> "$BIN"
    1.14      chmod +x "$BIN"
    1.15    done
    1.16 -  for NAME in Isabelle isabelle
    1.17 -  do
    1.18 -    BIN="$BINDIR/$NAME"
    1.19 -    echo "installing $BIN"
    1.20 -    rm -f "$BIN"
    1.21 -    cp "$ISABELLE_HOME/bin/$NAME" "$BIN" || fail "Cannot write file: $BIN"
    1.22 -    chmod +x "$BIN"
    1.23 -  done
    1.24  fi