Rev 41 | Show entire file | Regard whitespace | Details | Blame | Last modification | View Log | RSS feed
Rev 41 | Rev 43 | ||
---|---|---|---|
Line 30... | Line 30... | ||
30 | # `abort-remove' or `abort-deconfigure'. |
30 | # `abort-remove' or `abort-deconfigure'. |
31 | LOCAL_DIRS="share/pike/site_pike share/pike${PIKE}/site_pike lib/pike/site_pike lib/pike${PIKE}/site_pike include/pike include/pike${PIKE}" |
31 | LOCAL_DIRS="share/pike/site_pike share/pike${PIKE}/site_pike lib/pike/site_pike lib/pike${PIKE}/site_pike include/pike include/pike${PIKE}" |
32 | 32 | ||
33 | case "$1" in |
33 | case "$1" in |
34 | configure) |
34 | configure) |
35 | update-alternatives --install /usr/bin/pike pike /usr/bin/${PIKEBIN} 10 \ |
35 | update-alternatives --install /usr/bin/pike pike /usr/bin/${PIKEBIN} 12 \ |
36 | --slave /usr/share/man/man1/pike.1.gz pike.1.gz /usr/share/man/man1/${PIKEBIN}.1.gz |
36 | --slave /usr/share/man/man1/pike.1.gz pike.1.gz /usr/share/man/man1/${PIKEBIN}.1.gz |
37 | # |
37 | # |
38 | # If the creation fails, so be it, user might have the filesystem mounted r/o |
38 | # If the creation fails, so be it, user might have the filesystem mounted r/o |
39 | # |
39 | # |
40 | for d in $LOCAL_DIRS; do |
40 | for d in $LOCAL_DIRS; do |