more robust run of makeindex (amending 0f0a2148a099, Gerwin Klein 2004), using the old status-quo of e.g. doc-src/Intro/Makefile;
#!/usr/bin/env bash
set -e
FORMAT="$1"
VARIANT="$2"
isabelle latex -o "$FORMAT"
isabelle latex -o bbl
isabelle latex -o "$FORMAT"
isabelle latex -o "$FORMAT"
./isa-index root
isabelle latex -o "$FORMAT"