rename man9 => 9man

sorry

1 files changed, 0 insertions, 43 deletions

diff --git a/bin/man9 b/bin/man9
deleted file mode 100755
index cbbbd6e4..00000000
--- a/bin/man9
+++ /dev/null
@@ -1,43 +0,0 @@
-#! /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
-