equal
deleted
inserted
replaced
93 esac |
93 esac |
94 |
94 |
95 if [ -n "$BINDIR" ]; then |
95 if [ -n "$BINDIR" ]; then |
96 mkdir -p "$BINDIR" || fail "Bad directory: $BINDIR" |
96 mkdir -p "$BINDIR" || fail "Bad directory: $BINDIR" |
97 |
97 |
98 for NAME in isatool isabelle Isabelle |
98 for NAME in isatool isabelle-process isabelle-interface |
99 do |
99 do |
100 BIN="$BINDIR/$NAME" |
100 BIN="$BINDIR/$NAME" |
101 DIST="$DISTDIR/bin/$NAME" |
101 DIST="$DISTDIR/bin/$NAME" |
102 echo "installing $BIN" |
102 echo "installing $BIN" |
103 echo "#!$BASH" > "$BIN" || fail "Cannot write file: $BIN" |
103 echo "#!$BASH" > "$BIN" || fail "Cannot write file: $BIN" |
104 echo >> "$BIN" |
104 echo >> "$BIN" |
105 echo "exec \"$DIST\" \"\$@\"" >> "$BIN" |
105 echo "exec \"$DIST\" \"\$@\"" >> "$BIN" |
|
106 chmod +x "$BIN" |
|
107 done |
|
108 for NAME in Isabelle isabelle |
|
109 do |
|
110 BIN="$BINDIR/$NAME" |
|
111 DIST="$DISTDIR/bin/$NAME" |
|
112 echo "installing $BIN" |
|
113 cp "$DIST" "$BIN" || fail "Cannot write file: $BIN" |
106 chmod +x "$BIN" |
114 chmod +x "$BIN" |
107 done |
115 done |
108 fi |
116 fi |
109 |
117 |
110 |
118 |
136 |
144 |
137 echo "installing $KDEAPP" |
145 echo "installing $KDEAPP" |
138 echo "# KDE Config File" > "$KDEAPP" || fail "Cannot write file: $KDEAPP" |
146 echo "# KDE Config File" > "$KDEAPP" || fail "Cannot write file: $KDEAPP" |
139 echo "[KDE Desktop Entry]" >> "$KDEAPP" |
147 echo "[KDE Desktop Entry]" >> "$KDEAPP" |
140 echo "Type=Application" >> "$KDEAPP" |
148 echo "Type=Application" >> "$KDEAPP" |
141 echo "Exec=\"$DISTDIR/bin/Isabelle\" %f" >> "$KDEAPP" |
149 echo "Exec=\"$DISTDIR/bin/isabelle-interface\" %f" >> "$KDEAPP" |
142 echo "Icon=isabelle.xpm" >> "$KDEAPP" |
150 echo "Icon=isabelle.xpm" >> "$KDEAPP" |
143 echo "TerminalOptions=" >> "$KDEAPP" |
151 echo "TerminalOptions=" >> "$KDEAPP" |
144 echo "Path=" >> "$KDEAPP" |
152 echo "Path=" >> "$KDEAPP" |
145 echo "Terminal=0" >> "$KDEAPP" |
153 echo "Terminal=0" >> "$KDEAPP" |
146 echo "Name=Isabelle" >> "$KDEAPP" |
154 echo "Name=Isabelle" >> "$KDEAPP" |