1.1 --- a/doc-src/IsarImplementation/makeglossary Wed Mar 04 11:05:02 2009 +0100 1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 1.3 @@ -1,6 +0,0 @@ 1.4 -#!/bin/sh 1.5 -# $Id$ 1.6 - 1.7 -NAME="$1" 1.8 -makeindex -s nomencl -o "${NAME}.gls" "${NAME}.glo" 1.9 -./checkglossary "${NAME}.glo"