Skip to content
Browse files

Let IDE implementors (Toolbox, VSCode extensions, ...) pass an

identifier to the execution statistics collection.

"-Dtlc2.TLC.ide=toolbox" to report "toolbox" as IDE.

  • Loading branch information
lemmy committed Dec 1, 2019
1 parent 354d0e1 commit fe636624af94a06f943d6d4cd759803b3cea90eb
Showing with 4 additions and 1 deletion.
  1. +4 −1 tlatools/src/tlc2/
@@ -1147,8 +1147,11 @@ private void printStartupBanner(final int mode, final Map<String, String> parame

// True if TLC is run from within the Toolbox.
// True if TLC is run from within the Toolbox. Derive ide name from .tool too
// unless set explicitly. Eventually, we can probably remove the toolbox
// parameter.
udc.put("toolbox", Boolean.toString(TLCGlobals.tool));
udc.put("ide", System.getProperty(TLC.class.getName() + ".ide", TLCGlobals.tool ? "toolbox" : "cli"));
new ExecutionStatisticsCollector().collect(udc);

0 comments on commit fe63662

Please sign in to comment.
You can’t perform that action at this time.