[php] microtime funktioniert nicht korrekt bei PHP 4.3.10-18

[bigg]

moin moin,

versuch mal mit den Parametern true und false zu arbeiten. True und False liefern
jeweils unterschiedliche Formate.

Diese Version sollte den gewünschten Effekt erzielen:

Code:

microtime(true);