json in head incorrectly set to 12hr time

The json script in the head of my event pages is incorrectly set to 12hr time. An event of mine that starts at 7pm is showing a “startDate” of 07:00, or 7am. It should have a startDate of 19:00. It was picked up by Google in their “Events” results and is showing the wrong event time to anyone who searches for it.

This json is printed by single_header() on line 771 of eventpost.php. It uses get_rich_result($event) on line 661 to build the data about the event. get_rich_result() uses a lowercase “h”, or 12 hour time, in the $time_format variable used to calculate the startDate and endDate. Changing it to a capital “H”, or 24 hour time, fixes it for me.