Dear Makarius, Thanks, I forgot about that option.
With "isabelle latex" in the specified directory the error boils down to: ./root.tex:31: Package pdftex.def Error: File `isabelle-eps-converted-to.pdf' n ot found. See the pdftex.def package documentation for explanation. Type H <return> for immediate help. ... Should isabelle-eps-converted-to.pdf exist on my system? cheers chris On 03/26/2018 01:26 PM, Makarius wrote: > On 26/03/18 09:33, Christian Sternagel wrote: >> >> I don't see a significant difference in output between my original >> >> isabelle build_doc system > >> *** Failed to build document in >> "/tmp/isabelle-griff/document_output1585848392449927242/system" >> >> and the suggested >> >> isabelle build -c -b System -o document=pdf -o document_output=output >> >> *** Failed to build document in >> "/home/griff/repos/tools/isabelle/src/Doc/System/output/system" >> >> I am still unclear on why "isabelle document" fails in both cases. > > The difference is the output directory. In the latter situation, you can > go there and inspect root.log or run pdflatex root manually. > > > Makarius > _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
