equal
deleted
inserted
replaced
47 build with optional ISABELLE_BIBTEX and ISABELLE_MAKEINDEX |
47 build with optional ISABELLE_BIBTEX and ISABELLE_MAKEINDEX |
48 |
48 |
49 . "pdflatex": as above, but use ISABELLE_PDFLATEX (legacy mode for |
49 . "pdflatex": as above, but use ISABELLE_PDFLATEX (legacy mode for |
50 special LaTeX styles) |
50 special LaTeX styles) |
51 |
51 |
52 . "build": delegate to the executable "./build pdf", using |
52 . "build": delegate to the executable "./build pdf" |
53 ISABELLE_LUALATEX by default |
|
54 |
53 |
55 The presence of a "build" command within the document output directory |
54 The presence of a "build" command within the document output directory |
56 explicitly requires document_build=build. Minor INCOMPATIBILITY, need to |
55 explicitly requires document_build=build. Minor INCOMPATIBILITY, need to |
57 adjust session ROOT options. |
56 adjust session ROOT options. |
58 |
57 |