#! /bin/sed -f # double-space.sed -- add a blank after each line # $Id: double-space.sed,v 1.1 1998/07/06 20:32:03 cdua Exp $ # Carlos Duarte, 980706 # from command line: sed G a\