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
Responsible:
Environment: linux
Synopsis: {DATE_TIME}.formatted_out does not work for "yyyy[0]mm[0]dd [0]hh[0]mi[0]ss"

Description
"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