#!/bin/bash
## For the curious: "pager $1" doesn't work in batch, because "more" will
## eat the rest of stdin.  The no-argument version is intended for use at
## the end of a pipeline.
##
## PAGER is determined at configure time and recorded in `etc/Renviron'.
if test -n "${1}"; then
  exec ${PAGER} < ${1}
else
  exec ${PAGER}
fi

### Local Variables: ***
### mode: sh ***
### sh-indentation: 2 ***
### End: ***