doc-src/IsarImplementation/makeglossary

"The Isabelle/Isar Implementation" manual;

+
−#!/bin/sh
+
−# $Id$
+
−
+
−NAME="$1"
+
−makeindex -s nomencl -o "${NAME}.gls" "${NAME}.glo"
+
−./checkglossary "${NAME}.glo"