Rev 30349 | Blame | Compare with Previous | Last modification | View Log | Download | RSS feed
out=$1 shift for rdfile in $*; do \ echo "% --- Source file: ${rdfile} ---"; cat ${rdfile}; echo; echo '\eof'; done > $out
out=$1
shift
for rdfile in $*; do \
echo "% --- Source file: ${rdfile} ---";
cat ${rdfile}; echo; echo '\eof';
done > $out