@@ -201,9 +201,9 @@
///Gives back the real time
double realTime() const {return rtime;}
};
TimeStamp operator*(double b,const TimeStamp &t)
inline TimeStamp operator*(double b,const TimeStamp &t)
{
return t*b;
}