JMP Time Formatting

[#1]

I can't get the time format to work.  According to the scripting guide the format "m/d/y h:m:s" is used for both 12hr and 24hr time... WTF?  Why would I ever want a function to willy nilly give one or the other answer?  How do I get this to work!  

time = today(); //3619617166
formattedTime = format(time, "m/d/y h:m:s");
print(formattedTime);  //"09/12/2018 5:12:46 PM"
//What I want: "09/12/2018 17:12:46"

There's some cryptic notes in the Scripting Guide that make me feel it chooses 12hr or 24hrs based on your computer settings, which is a terrible idea b/c I don't want my code to break on half of my users computers.

If formatting doesn't work, is there a simple work around?

[#2]

You can use Format Pattern to modify your date and this has most likely been JMPs solution as the wish list item has been set to Delivered.

Numeric Formats (jmp.com)

How do I apply Custom Date (and Duration) Formats in JMP?