| changeset 578 | a2e6b1dd487e |
| parent 515 | b9b3473327e3 |
| parent 494 | 097d7c4634ea |
| child 584 | 33c6b6e755cd |
| 16: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 |