Rev 30211 | Blame | 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