In article <1991May31.163100.20328 at cbnewsl.att.com> rbr at bonnie.ATT.COM (228-4197,ATTT) writes:
Why not use "ed(1)" as:
....
If you want to double space, use sed or awk. Both of these will do
the trick:
$ sed G < input > output
$ awk '{ print $0 "\n" }'
--
Kevin Kuehl
krk at cs.purdue.edu