5 echo 'ps-to-gifs.sh FILE.ps'
11 FILE
=`basename $1 .ps`
18 # generate the pixmap at twice the size, then rescale (for antialiasing)
19 cat $1 | gs
-q -sDEVICE=ppmraw \
20 -sOutputFile="|pnmscale 0.5|ppmtogif > $FILE-page%d.gif" \
21 -r200 -dNOPAUSE - -c quit