time_t always an integer?

[Asko Kauppi <askok@...>]

I sent a separate mail to Lua authors on this, but... a more common  
survey wouldn't hurt? :)

Lua 5.1 beta still uses "pushNumber" in the os.time() function, but  
as far as I know, any 'time_t' is always an integer, albeit the  
interpretation of that value may differ. Is this right?

In other words, there is no system anywhere, that'd use 'float' or  
'double' for time_t.

If so, the return of os.time() should imho use "pushInteger()", which  
does make a difference on float/int32 patched systems, where pushing  
an integer allows full 32-bit range, but pushing a number (float)  
does not.

Small thing, unless one stumbles accross it.. (and one does, since  
current time_t values are outside of float range, so values change  
only every now and then, not by each second)

thanks for opinions,
-asko