Stream: Beginner Questions

Topic: isabelle document


view this post on Zulip Gergely Buday (Jul 19 2022 at 09:03):

From a previous run I am able to run my build script in $SESSION/output/document, but when I run

$ isabelle document -d .

I get

Bad file root.tex

My Isabelle 2020 does not have a verbose option for isabelle document so I do not see what's going on. I prepared this article last time with Isabelle 2020. How can I check what the problem is with my root.tex?


Last updated: Mar 29 2024 at 12:28 UTC