equal
deleted
inserted
replaced
59 |
59 |
60 ## main |
60 ## main |
61 |
61 |
62 mkdir -p "$BINDIR" || fail "Bad directory: $BINDIR" |
62 mkdir -p "$BINDIR" || fail "Bad directory: $BINDIR" |
63 |
63 |
64 BASH=$(type -path bash) |
64 #set by configure |
65 [ -z "$BASH" ] && fail "Cannot find bash!" |
65 AUTO_BASH=/bin/bash |
66 |
66 |
67 echo "using $DISTDIR" |
67 echo "using $DISTDIR" |
68 |
68 |
69 for NAME in isatool isabelle Isabelle |
69 for NAME in isatool isabelle Isabelle |
70 do |
70 do |
71 BIN="$BINDIR/$NAME" |
71 BIN="$BINDIR/$NAME" |
72 DIST="$DISTDIR/bin/$NAME" |
72 DIST="$DISTDIR/bin/$NAME" |
73 echo "installing $BIN" |
73 echo "installing $BIN" |
74 echo "#!$BASH" >$BIN || fail "Cannot write file: $BIN" |
74 echo "#!$AUTO_BASH" >$BIN || fail "Cannot write file: $BIN" |
75 echo >>$BIN |
75 echo >>$BIN |
76 echo "exec $DIST \"\$@\"" >>$BIN |
76 echo "exec $DIST \"\$@\"" >>$BIN |
77 chmod +x $BIN |
77 chmod +x $BIN |
78 done |
78 done |