You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Error running tla2tex.TLA (exit code 1) Exception in thread "main" tla2tex.TLA2TexException: TLATeX unrecoverable error: -- Trying to run the command `latex example.tex' produced the following error Cannot run program "latex": error=2, No such file or directory. at tla2tex.Debug.ReportError(Debug.java:26) at tla2tex.ExecuteCommand.executeCommand(ExecuteCommand.java:34) at tla2tex.LaTeXOutput.RunLaTeX(LaTeXOutput.java:483) at tla2tex.TLA.runTranslation(TLA.java:246) at tla2tex.TLA.main(TLA.java:150)
Where do I set the path for Latex? I have set the path for pdflatex correctly and I can run it from the terminal and convert the .tex file to PDF.
The text was updated successfully, but these errors were encountered:
Error running tla2tex.TLA (exit code 1) Exception in thread "main" tla2tex.TLA2TexException: TLATeX unrecoverable error: -- Trying to run the command `latex example.tex' produced the following error Cannot run program "latex": error=2, No such file or directory. at tla2tex.Debug.ReportError(Debug.java:26) at tla2tex.ExecuteCommand.executeCommand(ExecuteCommand.java:34) at tla2tex.LaTeXOutput.RunLaTeX(LaTeXOutput.java:483) at tla2tex.TLA.runTranslation(TLA.java:246) at tla2tex.TLA.main(TLA.java:150)
Where do I set the path for Latex? I have set the path for pdflatex correctly and I can run it from the terminal and convert the .tex file to PDF.
The text was updated successfully, but these errors were encountered: