Use new Time class in timed_wait()
authorMarco Costalba <mcostalba@gmail.com>
Sat, 3 Mar 2012 17:53:37 +0000 (18:53 +0100)
committerMarco Costalba <mcostalba@gmail.com>
Mon, 5 Mar 2012 18:18:46 +0000 (19:18 +0100)
commit482b5b7ecebc85e427c2c839337c7a893ae3e402
treee7c7bffbf6288b0e26284897863492cdd023a461
parent19540c9ee824abc156d5a12ab353c250a083da4b
Use new Time class in timed_wait()

And simplify the code.

No functional change.

Signed-off-by: Marco Costalba <mcostalba@gmail.com>
src/misc.cpp
src/misc.h
src/types.h