isabelle: src/Doc/Intro/document/build@5a14f2cc1ea0 (annotated)

53498 05313b45a5ae more portable hash-bang; wenzelm parents: 48985 diff changeset	1	#!/usr/bin/env bash
48971 5a4bcf466156 prepare document more uniformly; wenzelm parents: diff changeset	2
5a4bcf466156 prepare document more uniformly; wenzelm parents: diff changeset	3	set -e
5a4bcf466156 prepare document more uniformly; wenzelm parents: diff changeset	4
73740 c46ff0efa1ce more direct use of latex tools: avoid diversion into "isabelle latex -o pdf" and its confusion of ISABELLE_PDFLATEX vs. ISABELLE_LUALATEX; wenzelm parents: 73733 diff changeset	5	$ISABELLE_LUALATEX root
73733 b13b2c1d419e more robust run of makeindex (amending 0f0a2148a099, Gerwin Klein 2004), using the old status-quo of e.g. doc-src/Intro/Makefile; wenzelm parents: 73731 diff changeset	6
73742 c31510e70e95 proper bibliography; wenzelm parents: 73740 diff changeset	7	if [ -f manual.bib -o -f root.bib ]
73733 b13b2c1d419e more robust run of makeindex (amending 0f0a2148a099, Gerwin Klein 2004), using the old status-quo of e.g. doc-src/Intro/Makefile; wenzelm parents: 73731 diff changeset	8	then
73740 c46ff0efa1ce more direct use of latex tools: avoid diversion into "isabelle latex -o pdf" and its confusion of ISABELLE_PDFLATEX vs. ISABELLE_LUALATEX; wenzelm parents: 73733 diff changeset	9	$ISABELLE_BIBTEX root
c46ff0efa1ce more direct use of latex tools: avoid diversion into "isabelle latex -o pdf" and its confusion of ISABELLE_PDFLATEX vs. ISABELLE_LUALATEX; wenzelm parents: 73733 diff changeset	10	$ISABELLE_LUALATEX root
73733 b13b2c1d419e more robust run of makeindex (amending 0f0a2148a099, Gerwin Klein 2004), using the old status-quo of e.g. doc-src/Intro/Makefile; wenzelm parents: 73731 diff changeset	11	fi
b13b2c1d419e more robust run of makeindex (amending 0f0a2148a099, Gerwin Klein 2004), using the old status-quo of e.g. doc-src/Intro/Makefile; wenzelm parents: 73731 diff changeset	12
73740 c46ff0efa1ce more direct use of latex tools: avoid diversion into "isabelle latex -o pdf" and its confusion of ISABELLE_PDFLATEX vs. ISABELLE_LUALATEX; wenzelm parents: 73733 diff changeset	13	$ISABELLE_LUALATEX root
73733 b13b2c1d419e more robust run of makeindex (amending 0f0a2148a099, Gerwin Klein 2004), using the old status-quo of e.g. doc-src/Intro/Makefile; wenzelm parents: 73731 diff changeset	14
b13b2c1d419e more robust run of makeindex (amending 0f0a2148a099, Gerwin Klein 2004), using the old status-quo of e.g. doc-src/Intro/Makefile; wenzelm parents: 73731 diff changeset	15	if [ -f root.idx ]
b13b2c1d419e more robust run of makeindex (amending 0f0a2148a099, Gerwin Klein 2004), using the old status-quo of e.g. doc-src/Intro/Makefile; wenzelm parents: 73731 diff changeset	16	then
b13b2c1d419e more robust run of makeindex (amending 0f0a2148a099, Gerwin Klein 2004), using the old status-quo of e.g. doc-src/Intro/Makefile; wenzelm parents: 73731 diff changeset	17	"$ISABELLE_HOME/src/Doc/sedindex" root
73740 c46ff0efa1ce more direct use of latex tools: avoid diversion into "isabelle latex -o pdf" and its confusion of ISABELLE_PDFLATEX vs. ISABELLE_LUALATEX; wenzelm parents: 73733 diff changeset	18	$ISABELLE_LUALATEX root
73733 b13b2c1d419e more robust run of makeindex (amending 0f0a2148a099, Gerwin Klein 2004), using the old status-quo of e.g. doc-src/Intro/Makefile; wenzelm parents: 73731 diff changeset	19	fi

author	desharna
	Wed, 18 Oct 2023 10:41:12 +0200
changeset 78788	5a14f2cc1ea0
parent 73772	6b4c47666267
permissions	-rwxr-xr-x