New global JS functions: file_getdosname() returns the Micros~1 shortened

version of the specified path/filename on Windows, the unmodified path/filename
on other platforms.