| changeset 383 | 097d7c4634ea |
| parent 368 | 879c55700cd4 |
| child 427 | c59bdcc8e33e |
| 12:13ebd5cc32ad | 13: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 |