On 2020-10-26, at 22:16, Brian E Carpenter <brian.e.carpenter@xxxxxxxxx> wrote: > > Maybe it's because I was brought up on paper tape rather than punch cards, Ah! I used both in the 1970s, but more punch cards, and even my paper tape was mostly Z-folded not rolled… That explains it. > but I can't see why anybody cares about pagination in 2020. Proof by lack of imagination :-) Apparently these people do exist, and they have been speaking up with their use cases. Grüße, Carsten
