src/Doc/Intro/document/build
author wenzelm
Sun, 05 Feb 2023 20:09:39 +0100
changeset 77199 7d7786585ab0
parent 73772 6b4c47666267
permissions -rwxr-xr-x
more diagnostic operations (see also 5c7652e9bc01);

#!/usr/bin/env bash

set -e

$ISABELLE_LUALATEX root

if [ -f manual.bib -o -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