我开始了探索 TLA+ 和更正式的软件工程的旅程。我正在使用 TLA Toolbox 版本 1.6.0，但是，我注意到内置文档和在线文档都没有提供有关如何编辑或设置自动生成的修改历史日志中使用的默认“作者姓名”的任何提示。
例如，在我当前的机器上，日志采用以下形式...
\* Modification History
\* Last modified Sat Jan 11 12:21:35 EAT 2020 by GAMER
那个“GAMER”是我想要修改的字符串——比如说，我的首字母。但是，尽管您可以手动编辑该名称内联 - 在模块编辑器中，当您保存此更改时，新的修改注释会插入到历史记录中，但之前的错误相同！
如何解决这个问题？使用了一些环境变量？配置文件或注册表值？我会理解它可能会读取系统用户信息左右，但这也不是我的系统用户名！