Wed, 19 May 2021 11:54:58 +0200 more direct use of latex tools: avoid diversion into "isabelle latex -o pdf" and its confusion of ISABELLE_PDFLATEX vs. ISABELLE_LUALATEX;
wenzelm [Wed, 19 May 2021 11:54:58 +0200] rev 73740
more direct use of latex tools: avoid diversion into "isabelle latex -o pdf" and its confusion of ISABELLE_PDFLATEX vs. ISABELLE_LUALATEX; clarified ISABELLE_MAKEINDEX options;
Wed, 19 May 2021 11:48:35 +0200 default document_build (lualatex);
wenzelm [Wed, 19 May 2021 11:48:35 +0200] rev 73739
default document_build (lualatex);
Wed, 19 May 2021 11:18:38 +0200 more robust: allow \printindex within the document;
wenzelm [Wed, 19 May 2021 11:18:38 +0200] rev 73738
more robust: allow \printindex within the document;
(0) -30000 -10000 -3000 -1000 -300 -100 -30 -10 -3 +3 +10 +30 +100 +300 +1000 tip