#!/bin/csh -f

# Doublespace standard input or filename arguments to standard output

cat $* | awk '{print $0; print ""}'