diff --git a/doc/makeglos b/doc/makeglos new file mode 100755 index 0000000000..00723d0631 --- /dev/null +++ b/doc/makeglos @@ -0,0 +1,2 @@ +#!/bin/sh +makeindex -s $1.ist -t $1.glg -o $1.gls $1.glo