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

Christian Müller's avatar
Christian Müller committed
6
7
8
9
10
11

echo "Gobbling up metrics"

rm -f results/allmetrics.metrics
touch results/allmetrics.metrics

12
for FILE in results/**/*.metrics
Christian Müller's avatar
Christian Müller committed
13
14
15
16
17
18
do
	echo "${FILE}:" >> results/allmetrics.metrics
	cat ${FILE} >> results/allmetrics.metrics
	echo -e "\n\n" >> results/allmetrics.metrics
done

19
for FILE in results/**/*.png
Christian Müller's avatar
Christian Müller committed
20
do
Christian Müller's avatar
Christian Müller committed
21
	echo "Deleting ${FILE}"
Christian Müller's avatar
Christian Müller committed
22
23
24
	rm $FILE
done

25
for FILE in results/**/*.dot
Christian Müller's avatar
Christian Müller committed
26
27
28
29
30
31
32
33
34
35
36
37
38
39
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