How to edit or set the TLA+ Toolbox Module Modification History Comment syntax or parameters?

Question

Am starting my journey exploring TLA+ and more formal software engineering. Am using TLA Toolbox version 1.6.0, however, I notice that neither the inbuilt docs, nor the online docs offer any hints on how to go about editing or setting the default "Author name" used in the auto-generated modification history log.

For example, on my current machine, the logs take the form below...

\* Modification History
\* Last modified Sat Jan 11 12:21:35 EAT 2020 by GAMER

That "GAMER" is the string I wish to modify - say, to my initials. However, though you can manually edit that name inline - in the module editor, immediate you save this change, a new modification comment is inserted into the history with the same former mistake!

How to remedy this? Some environment variable used? A config file or registry value? I would understand that perhaps it reads the system user info or so, but that's not what I have as my system user name either!

Answer 1

./toolbox --launcher.appendVmargs -vmargs -Duser.name=nemesisfixx