equal
deleted
inserted
replaced
44 |
44 |
45 ### |
45 ### |
46 ### Document preparation (cf. isabelle latex/document) |
46 ### Document preparation (cf. isabelle latex/document) |
47 ### |
47 ### |
48 |
48 |
49 ISABELLE_LATEX="latex" |
49 ISABELLE_LATEX="latex -file-line-error" |
50 ISABELLE_PDFLATEX="pdflatex" |
50 ISABELLE_PDFLATEX="pdflatex -file-line-error" |
51 ISABELLE_BIBTEX="bibtex" |
51 ISABELLE_BIBTEX="bibtex" |
52 ISABELLE_MAKEINDEX="makeindex" |
52 ISABELLE_MAKEINDEX="makeindex" |
53 ISABELLE_EPSTOPDF="epstopdf" |
53 ISABELLE_EPSTOPDF="epstopdf" |
|
54 |
|
55 if [ "$ISABELLE_PLATFORM_FAMILY" = "windows" ]; then |
|
56 ISABELLE_LATEX="latex -c-style-errors" |
|
57 ISABELLE_PDFLATEX="pdflatex -c-style-errors" |
|
58 fi |
54 |
59 |
55 |
60 |
56 ### |
61 ### |
57 ### Misc path settings |
62 ### Misc path settings |
58 ### |
63 ### |