rename man9 => 9man

sorry

1 files changed, 43 insertions, 0 deletions

diff --git a/bin/9man b/bin/9man
new file mode 100755
index 00000000..cbbbd6e4
--- /dev/null
+++ b/bin/9man
@@ -0,0 +1,43 @@
+#! /bin/sh
+root=$PLAN9/man
+
+while [ $# -gt 0 ] ; do
+    case $1 in
+	[0-9]) sec="$sec $1" ;;
+	*) break ;;
+    esac
+    shift
+done
+
+if [ "X$sec" = "X" ] ; then
+    sec=`ls -d $root/man[0-9]* | sed -e 's;/$;;' -e 's;^.*/man;;'`
+fi
+
+pat='^('`echo $* | sed -e 's; ;|;g'`')' ;
+for s in $sec ; do
+    if [ -f $root/$s/INDEX ] ; then
+	try=`grep -E $pat $root/man$s/INDEX | sed -e 's;^[^ ]* ;;'` ;
+    fi
+    if [ "X$try" != "X" ] ; then
+	for f in $try ; do
+	    files="$files $root/man$s/$f.$s";
+	done
+	try="";
+    fi
+    for f in $* ; do
+	if [ -f $root/man$s/$f.$s ] ; then
+	    files="$files $root/man$s/$f.$s" ;
+	fi
+    done
+done 
+
+files=`echo $files | tr ' ' '\n' | sort -u`;
+
+if [ "X$files" = "X" ] ; then
+    echo "No manual entry for $*";
+    exit 1;
+fi
+
+exmac=".de EX\n.ift .ft 5\n.nf\n..\n.de EE\n.ft1\n.fi\n.."
+( echo -e $exmac ; cat $files ) | nroff -man
+