+ --logfile "${buildfile}" \
+ $options \
+ "$@" && status='OK' || { status='FAILED'; failed=1; }
+ timeinfo=$(tail -n 1 "${tsfile}")
+ # Update the summary of builds
+ touch summary.build # Assure existence
+ sed -i -e "s/\(${buildfile}.*out$\)/\1 OLD/g" summary.build # Mark previous entry as OLD
+ echo -e "${buildfile}\t$status\t$timeinfo" >> summary.build # Add current one
+ rm -f "${tsfile}"