--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarImplementation/makeglossary Mon Jan 02 20:16:52 2006 +0100
@@ -0,0 +1,6 @@
+#!/bin/sh
+# $Id$
+
+NAME="$1"
+makeindex -s nomencl -o "${NAME}.gls" "${NAME}.glo"
+./checkglossary "${NAME}.glo"