src/Doc/prepare_document
author wenzelm
Wed, 19 May 2021 11:54:58 +0200
changeset 73740 c46ff0efa1ce
parent 73733 b13b2c1d419e
child 73742 c31510e70e95
permissions -rwxr-xr-x
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;

#!/usr/bin/env bash

set -e

$ISABELLE_LUALATEX root

if [ -f root.bib ]
then
  $ISABELLE_BIBTEX root
  $ISABELLE_LUALATEX root
fi

$ISABELLE_LUALATEX root

if [ -f root.idx ]
then
  "$ISABELLE_HOME/src/Doc/sedindex" root
  $ISABELLE_LUALATEX root
fi