changeset 505 | 097d7c4634ea |
parent 491 | 879c55700cd4 |
child 548 | 94387da47f79 |
14:13ebd5cc32ad | 16:b1b2707c8120 |
---|---|
200 } |
200 } |
201 ///Gives back the real time |
201 ///Gives back the real time |
202 double realTime() const {return rtime;} |
202 double realTime() const {return rtime;} |
203 }; |
203 }; |
204 |
204 |
205 TimeStamp operator*(double b,const TimeStamp &t) |
205 inline TimeStamp operator*(double b,const TimeStamp &t) |
206 { |
206 { |
207 return t*b; |
207 return t*b; |
208 } |
208 } |
209 |
209 |
210 ///Prints the time counters |
210 ///Prints the time counters |