tool.sh (737B)
1 #!/bin/sh 2 3 if [ -z "$TOOL" ]; then 4 echo "No tool selected (TOOL variable must be set)" 5 exit 1 6 fi 7 8 CC="$CC -D_POSIX_C_SOURCE=199309L" # For timer 9 10 BIN="tools/run" 11 RESULTS="tools/results" 12 LAST="$RESULTS/last.out" 13 date="$(date +'%Y-%m-%d-%H-%M-%S')" 14 15 for t in tools/*; do 16 if [ ! -d "$t" ] || ! (echo "$t" | grep -q "$TOOL"); then 17 continue 18 fi 19 toolname="$(basename "$t" .c)" 20 break 21 done 22 23 file="$RESULTS/$toolname-$date.txt" 24 25 $CC -o $BIN "$t"/*.c "$OBJ" || exit 1; 26 27 ( 28 date +'%Y-%m-%d %H:%M' 29 echo "" 30 echo "======== config.mk ========" 31 cat config.mk 32 echo "" 33 echo "=== tool configuration ====" 34 echo "TOOL=$toolname" 35 echo "TOOLARGS=$TOOLARGS" 36 echo "CC=$CC" 37 echo "" 38 echo "======= tool output =======" 39 $BIN $TOOLARGS 40 ) | tee "$file" "$LAST"