renderpngs.sh 415 Bytes
Newer Older
Christian Müller's avatar
Christian Müller committed
1 2 3 4
# /bin/bash
shopt -s nullglob
TIMEOUT=1m

Christian Müller's avatar
Christian Müller committed
5 6
for FILE in results/*/*.png
do
Christian Müller's avatar
Christian Müller committed
7
	echo "Deleting ${FILE}"
Christian Müller's avatar
Christian Müller committed
8 9 10
	rm $FILE
done

Christian Müller's avatar
Christian Müller committed
11 12 13 14 15 16 17 18 19 20 21 22 23 24 25
for FILE in results/*/*.dot
do
	NAME=$(basename ${FILE} .dot)
	DIR=$(dirname "${FILE}")
	PIC="${DIR}/${NAME}.png"

	echo "Rendering ${FILE} to ${PIC}"
	if
		timeout ${TIMEOUT} time -p dot -Tpng < ${FILE} >> ${PIC} 
	then
		echo "Finished successfully"
	else
		echo "Timeout after ${TIMEOUT}"
	fi
done