diff --git a/language/predefined/variables/server.xml b/language/predefined/variables/server.xml
index e37f07e634..9b09055db2 100644
--- a/language/predefined/variables/server.xml
+++ b/language/predefined/variables/server.xml
@@ -156,7 +156,16 @@
The timestamp of the start of the request. Available since PHP 5.1.0.
- It is float with microseconds since PHP 5.4.0.
+
+
+
+
+
+ 'REQUEST_TIME_FLOAT'
+
+
+ The timestamp of the start of the request, with microsecond precision.
+ Available since PHP 5.4.0.