11 echo "1234567890 $op $i" > "files-$op-2/$i"
18 { time ../src/tdatp1 "$F" "$F.out";} 2> "$F.time";
24 F="files-$op-2/$i.time"
25 RT=`cat $F | grep real | cut -d ' ' -f 2`
26 RT=`echo $RT | cut -d 'm' -f 2 | cut -d 's' -f 1`
27 echo "$i $RT" >> "files-$op-2/times"