#!/bin/sh -x M1=`make path` time() { sed '/^.*of \([0-9.]*\) seconds.*/s//\1/p;d'