src/Doc/Tutorial/document/build
author wenzelm
Sun, 04 Aug 2024 17:39:47 +0200
changeset 80636 4041e7c8059d
parent 73740 c46ff0efa1ce
permissions -rwxr-xr-x
tuned: more explicit dest_Const_name and dest_Const_type;

#!/usr/bin/env bash

set -e

$ISABELLE_LUALATEX root
$ISABELLE_BIBTEX root
$ISABELLE_LUALATEX root
$ISABELLE_LUALATEX root
./isa-index root
$ISABELLE_LUALATEX root