PR# 19407 {DATE_TIME}.formatted_out does not work for "yyyy[0]mm[0]dd [0]hh[0]mi[0]ss"

Problem Report Summary
Submitter: finnianr
Category: EiffelTime
Priority: Low
Date: 2017/11/17
Class: Bug
Severity: Non-critical
Number: 19407
Release: 16.05
Confidential: No
Status: Open
Environment: linux
Synopsis: {DATE_TIME}.formatted_out does not work for "yyyy[0]mm[0]dd [0]hh[0]mi[0]ss"

"yyyy[0]mm[0]dd [0]hh[0]mi[0]ss" should be a legitimate format string for {DATE_TIME}.formatted_out, but the result is incorrect!. I just get "02 02" if the time is initialized as: 11/17/2017 14:24:13

However if I just use either the date part or the time part on it's own, I get correct results.

Ideally what I need is an ISO-8601 date format which would be "yyyy[0]mm[0]ddT[0]hh[0]mi[0]ssZ", but this won't work either.
To Reproduce

Problem Report Interactions
From:finnianr    Date:2017/11/18    Status: Open    Download   
There is a corresponding problem with {DATE_TIME}.make_string