#! /bin/csh -f
#
#    Starts up xman with the tools manual pages
#
if ($?PXDIR == 0) set PXDIR = "/home/gropp/pexec"
(setenv MANPATH $PXDIR/man ; xman -notopbox $* )
