Gergely Buday (Jul 19 2022 at 09:03): 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: Dec 21 2024 at 16:20 UTC