#! /bin/sed -f
### doublespace READS FROM STANDARD INPUT OR FROM FILE(S), AND
### DOUBLE-SPACES THEM ONTO STANDARD OUTPUT.
G
