| changeset 540 | 9d0d7e20f76d |
| parent 492 | b9b3473327e3 |
| parent 536 | 097d7c4634ea |
| child 576 | 33c6b6e755cd |
| 15:f6f29b389758 | 17:1220bc45d43f |
|---|---|
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 |