diff options
Diffstat (limited to 'sdk/bin/instman')
| -rwxr-xr-x | sdk/bin/instman | 32 |
1 files changed, 32 insertions, 0 deletions
diff --git a/sdk/bin/instman b/sdk/bin/instman new file mode 100755 index 0000000..d8ca6f7 --- /dev/null +++ b/sdk/bin/instman @@ -0,0 +1,32 @@ +#!/bin/sh +prefix=$1 +set=$2 +shift +shift + +for page in $* ; do + source=$page'.'$set + target="" + if [ -d $prefix/man$set ] ; then + mandir=$prefix/man$set + target=$mandir/$page'.'$set + fi + if [ -z $target ] ; then + roff=nroff + if [ -f /usr/lib/groff ] ; then + roff="groff -Tascii" + fi + if [ -f /usr/local/lib/groff ] ; then + roff="groff -Tascii" + fi + if [ -d $prefix/cat$set ] ; then + mandir=$prefix/cat$set + target=$mandir/$page.set + $roff -man <$source >$page'.man' + source=$page'.man' + fi + fi + echo 'Adding '$page' to '$mandir + install -g man -m 0664 $source $target +done + |