How to Add a New Module Dependency in VSCode TLA?

TLA+ has community modules that user modules can extend from. The Github repository tlaplus/CommunityModules houses these community modules. The community modules are packaged as a jar file. If you are using TLA Toolbox, then you can add the jar file in the classpath and use the community module in your TLA modules. The README files includes a link to a video that shows how you can include the module in your code.

If you are using VScode and its excellent TLA+ Plugin, then how do you include the jar file in your classpath?

It turns out that the plugin allows you to include custom jar files having external modules in your classpath. From the documentation:

If you provide a -cp or -classpath option that doesn’t explicitly contain a path to the tal2tools.jar library, the exstension will add the default class path to the end of the option value.