From ad5d9f69e0f29815bba9ecf68a0b89d0cde41039 Mon Sep 17 00:00:00 2001 From: loki der quaeler <loki@theori.st> Date: Tue, 18 Feb 2020 16:23:17 -0800 Subject: [PATCH] Changelog updates . Updating nomnolith sub-option. --- general/docs/changelogs/ch1_6_1.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/general/docs/changelogs/ch1_6_1.md b/general/docs/changelogs/ch1_6_1.md index e629d5af9..e1ce796d3 100644 --- a/general/docs/changelogs/ch1_6_1.md +++ b/general/docs/changelogs/ch1_6_1.md @@ -12,7 +12,7 @@ The high level changelog is available at http://research.microsoft.com/en-us/um/ * Running TLC with both the `-generateSpecTE` flag will enable 'tool mode' output and, in the event that the model check encounters errors, generate a `SpecTE.tla` and `SpecTE.cfg` file pair that captures the state trace reconstruction in an Init-Next relation spec. * This `SpecTE.tla` will, by default, be a monolithic file, prefaced by the tool output, followed a the `SpecTE` MODULE definition which includes all extended non-StandardModule TLA code as well. - * To prevent the monolith inclusion of dependent TLA code, specify `-nomonolith` + * To prevent the monolith inclusion of dependent TLA code, specify `nomonolith` after the `-generateSpecTE` * Running TLC with `-h` now displays a usage page reminiscent of a standard man page. * TraceExplorer exposes four capabilities: * running the TraceExplorer with no spec name puts the TraceExplorer into a mode to receive input via stdin (e.g in order to pipe tool-mode output from TLC) -- GitLab