#!/bin/sh
# This file is created by the CONFIGURE shell script.
# You should call it from the $SHOME/cmd/help script.

case $# in
1)    
;;
*)    
      echo "Usage: $0 help_file"
      exit 1
;;
esac

sed -e "/^\.ul/d
    /\`/s/\'//g
    /\`/s/\`//g" "$1" |
    nroff -Ttn300 $SHOME/cmd/help.nr - | lp || exit 1
    echo "Sent $1 to the printer."