Hi! On Fri, Oct 2, 2009 at 2:38 AM, Andreas Tille <[email protected]> wrote: > So the fix for this would probably be > > if [ -x /usr/bin/time ] ; then > TIME="time" > else > TIME="" > fi > echo "*** makevolume ***" > $TIME makevolume > echo "*** rendervolume ***" > $TIME rendervolume > ...
Can't we just change the header to use bash and let it use "time" as before? It's a test script (they can be bash scripts without any problems) and not an init script, for example. Best regards, Nelson -- To UNSUBSCRIBE, email to [email protected] with a subject of "unsubscribe". Trouble? Contact [email protected]
