- * @param $type String: can be 'date', 'time' or 'both'
- * @param $ts Mixed: the time format which needs to be turned into a
- * date('YmdHis') format with wfTimestamp(TS_MW,$ts)
- * @param $user User object used to get preferences for timezone and format
- * @param $options Array, can contain the following keys:
- * - 'timecorrection': time correction, can have the following values:
- * - true: use user's preference
- * - false: don't use time correction
- * - integer: value of time correction in minutes
- * - 'format': format to use, can have the following values:
- * - true: use user's preference
- * - false: use default preference
- * - string: format to use
+ * @param string $type Can be 'date', 'time' or 'both'
+ * @param mixed $ts The time format which needs to be turned into a
+ * date('YmdHis') format with wfTimestamp(TS_MW,$ts)
+ * @param User $user User object used to get preferences for timezone and format
+ * @param array $options Array, can contain the following keys:
+ * - 'timecorrection': time correction, can have the following values:
+ * - true: use user's preference
+ * - false: don't use time correction
+ * - int: value of time correction in minutes
+ * - 'format': format to use, can have the following values:
+ * - true: use user's preference
+ * - false: use default preference
+ * - string: format to use