void WriteIni(str FileName, str Section, str Key, any Value)
Writes the specified value to an INI file. The first parameter is the name of the INI file, the second is the name of a section in the INI file, and the third is the name of a key in the section. The last parameter should be set to the value you wish to be written to the INI file; it can be of any type.
A compiler error will be raised if the write fails.