# HG changeset patch # User wenzelm # Date 1621361942 -7200 # Node ID b13b2c1d419ef66e699a10667c7a3722c5302d54 # Parent 9b77e267e6a97abdaa85dc10ce4cee639ada404f more robust run of makeindex (amending 0f0a2148a099, Gerwin Klein 2004), using the old status-quo of e.g. doc-src/Intro/Makefile; diff -r 9b77e267e6a9 -r b13b2c1d419e src/Doc/Tutorial/document/build --- a/src/Doc/Tutorial/document/build Tue May 18 19:59:22 2021 +0200 +++ b/src/Doc/Tutorial/document/build Tue May 18 20:19:02 2021 +0200 @@ -7,6 +7,7 @@ isabelle latex -o "$FORMAT" isabelle latex -o bbl +isabelle latex -o "$FORMAT" +isabelle latex -o "$FORMAT" ./isa-index root isabelle latex -o "$FORMAT" -isabelle latex -o "$FORMAT" diff -r 9b77e267e6a9 -r b13b2c1d419e src/Doc/prepare_document --- a/src/Doc/prepare_document Tue May 18 19:59:22 2021 +0200 +++ b/src/Doc/prepare_document Tue May 18 20:19:02 2021 +0200 @@ -5,7 +5,17 @@ FORMAT="$1" isabelle latex -o "$FORMAT" -isabelle latex -o bbl -[ -f root.idx ] && "$ISABELLE_HOME/src/Doc/sedindex" root + +if [ -f root.bib ] +then + isabelle latex -o bbl + isabelle latex -o "$FORMAT" +fi + isabelle latex -o "$FORMAT" -isabelle latex -o "$FORMAT" + +if [ -f root.idx ] +then + "$ISABELLE_HOME/src/Doc/sedindex" root + isabelle latex -o "$FORMAT" +fi diff -r 9b77e267e6a9 -r b13b2c1d419e src/Pure/Thy/document_build.scala --- a/src/Pure/Thy/document_build.scala Tue May 18 19:59:22 2021 +0200 +++ b/src/Pure/Thy/document_build.scala Tue May 18 20:19:02 2021 +0200 @@ -348,14 +348,17 @@ List( "set -e", latex_bash(), - "if [ -f " + root_bash("bib") + " ]; then", + "if [ -f " + root_bash("bib") + " ]", + "then", " " + latex_bash("bbl"), - "fi", - "if [ -f " + root_bash("idx") + " ]; then", - " " + latex_bash("idx"), + " " + latex_bash(), "fi", latex_bash(), - latex_bash())) + "if [ -f " + root_bash("idx") + " ]", + "then", + " " + latex_bash("idx"), + " " + latex_bash(), + "fi")) } }