changeset 569 | 24682336c38e |
parent 492 | b9b3473327e3 |
parent 505 | 097d7c4634ea |
child 584 | 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 |