On Tue, 2007-05-01 at 12:43 +0200, Joerg Wunsch wrote:
> As Richard Earnshaw wrote:
>
> > > That's what I did, but it doesn't help for the non-standard usage
> > > of /usr/bin/time (-f option). They even explicitly used
> > > /usr/bin/time rather than bash's builtin.
>
> > No, it uses whichever time program you pass to the configure script
> > with the -S flag. So just install gnu time as .../gtime and
> > configure with -S .../gtime. R.
>
> [EMAIL PROTECTED] 2156% pwd
> /junk/CSiBE
> [EMAIL PROTECTED] 2157% find . -name configure
> [EMAIL PROTECTED] 2158% gtime
>
> CORRECT>time (y|n|e|a)?
>
.../bin/create-config
