blob: 7e09684631eee18d9b77c63c0ad1322c21c25d8f (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
|
#!/bin/sh
if [ -z "$TOOL" ]; then
echo "No tool selected (TOOL variable must be set)"
exit 1
fi
CC="$CC -D_POSIX_C_SOURCE=199309L"
BIN="tools/run"
d="$(date +'%Y-%m-%d-%H-%M-%S')"
for t in tools/*; do
if [ ! -d "$t" ] || ! (echo "$t" | grep -q "$TOOL"); then
continue
fi
toolname="$(basename "$t" .c)"
$CC -o $BIN "$t"/*.c "$CUBEOBJ" || exit 1;
$BIN | tee "tools/results/$toolname-$d.txt" "tools/results/last.out"
break
done
# $BIN is kept so it can be run manually for profiling
rm -rf "$CUBEOBJ"
|
