From c015b83de894d8c5d73b296f992ec4ced192ec0c Mon Sep 17 00:00:00 2001 From: loki der quaeler <quaeler@gmail.com> Date: Fri, 13 Mar 2020 15:19:24 -0700 Subject: [PATCH] TLC argument processing fails if -generateSpecTE is last argument . Discovered while working with the VS Code extension code. [Bug][Tools] --- tlatools/src/tlc2/TLC.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tlatools/src/tlc2/TLC.java b/tlatools/src/tlc2/TLC.java index 48c2d52d3..3d180a7ca 100644 --- a/tlatools/src/tlc2/TLC.java +++ b/tlatools/src/tlc2/TLC.java @@ -415,7 +415,7 @@ public class TLC { TLCGlobals.tool = true; - if (args[index].equals("nomonolith")) { + if ((index < args.length) && args[index].equals("nomonolith")) { index++; avoidMonolithSpecTECreation = true; } -- GitLab