# Shell-Skript (Linux bash) zur Umwandlung von dvi-Dateien in gif-Dateien
#
# Benutzt die programme sed,dvips,gs und ppmtogif
#
datei=`echo $1 | sed 's/.dvi$//g'`
dvips -i -S 1 $datei.dvi
for f in $datei.0*
do mv $f $f.ps
echo "quit" | gs -sDEVICE=ppmraw -sOutputFile="/home/jw/tmp/tmp.ppm" -dNOPAUSE -r140 $f.ps 
ppmtogif ~/tmp/tmp.ppm >$f.gif
rm -f ~/tmp/tmp.ppm
rm -f $f.ps
done