[OT] Awk question

[Rui Miguel Silva Seabra]

On Wed, Aug 20, 2008 at 11:03:58AM +0100, Dan Track wrote:
> Just wondering if you could lend me a little hand. Basically I want to
> rename a file from log.1 log.2 etc to log.10.36.34. The time stamp
> (ignore the date) should be the last written time, so far I've got to
> this stage:
> 
> stat log | sed  -n '/Modify:/p' | awk -F ' ' '{print $3}'
> 
> so I get :
> 11:01:09.000000000
> 
> How can I get rid of the leading 0'swithout having to pipe the output
> to anotehr awk statement, is it possible to do this withing the
> current awk statement?

There simpler solutions but this works:

stat log | awk '/Modify/ { print $3 }' | cut -d . -f 1

-- 
Wibble.
Today is Boomtime, the 13rd day of Bureaucracy in the YOLD 3174
+ No matter how much you do, you never do enough -- unknown
+ Whatever you do will be insignificant,
| but it is very important that you do it -- Gandhi
+ So let's do it...?