diff --git a/core/includes/bootstrap.inc b/core/includes/bootstrap.inc
index 9b4667e81d56b61a8f080efe80b3b8f69bedabf9..70bec28d0bbe03f0208e724b9cc77e5011c39279 100644
--- a/core/includes/bootstrap.inc
+++ b/core/includes/bootstrap.inc
@@ -198,10 +198,14 @@
 define('LANGUAGE_RTL', 1);
 
 /**
- * For convenience, define a short form of the request time global.
+ * Time of the current request in seconds elapsed since the Unix Epoch.
  *
- * REQUEST_TIME is a float with microseconds since PHP 5.4.0, but float
- * timestamps confuses most of the PHP functions (including date_create()).
+ * This differs from $_SERVER['REQUEST_TIME'], which is stored as a float
+ * since PHP 5.4.0. Float timestamps confuse most PHP functions
+ * (including date_create()).
+ *
+ * @see http://php.net/manual/reserved.variables.server.php
+ * @see http://php.net/manual/function.time.php
  */
 define('REQUEST_TIME', (int) $_SERVER['REQUEST_TIME']);