#! /bin/csh -f
# File  mani
# Last modified on Sun Mar 17 17:43:13 PST 1991 by stolfi
#================================================
man -i $*