def readfile(name, outstream, start=0, end=None):
    """Outputs the file at name to a stream.

        Data are copied starting from start. If end is not None,
        data are copied up to end.

        """
