Skip to content

Typo in the CLI page about TLC usage #92

@fgmarand

Description

@fgmarand

On the CLI page at https://www.learntla.com/topics/cli.html

The TLC syntax is given as

$ java -jar tla2tools.jar -config configfile.cfg specfile.tla

However, this is missing the TLC class, and should instead be:

$ java -jar tla2tools.jar tlc2.TLC -config configfile.cfg specfile.tla

The provided syntax causes this error, because it interprets the spec file as the name of the class to run :

Error: Could not find or load main class specfile.tla
Caused by: java.lang.ClassNotFoundException: specfile.tla

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions