equal
deleted
inserted
replaced
120 KDEDESKTOP=~/KDesktop |
120 KDEDESKTOP=~/KDesktop |
121 KDEAPP="$KDEDESKTOP/Isabelle.desktop" |
121 KDEAPP="$KDEDESKTOP/Isabelle.desktop" |
122 else |
122 else |
123 fail "Unknown KDE version \"$KDE\"" |
123 fail "Unknown KDE version \"$KDE\"" |
124 fi |
124 fi |
|
125 mkdir -p "$KDEDESKTOP" || fail "Bad directory: $KDEDESKTOP" |
125 |
126 |
126 KDEICONS="$KDEHOME/share/icons" |
127 KDEICONS="$KDEHOME/share/icons" |
127 mkdir -p "$KDEICONS" || fail "Bad directory: $KDEICONS" |
128 mkdir -p "$KDEICONS" || fail "Bad directory: $KDEICONS" |
128 mkdir -p "$KDEICONS/mini" || fail "Bad directory: $KDEICONS/mini" |
129 mkdir -p "$KDEICONS/mini" || fail "Bad directory: $KDEICONS/mini" |
129 |
130 |