diff --git a/tools/doc.pl b/tools/doc.pl index f4341b4..adc015f 100755 --- a/tools/doc.pl +++ b/tools/doc.pl @@ -283,4 +283,6 @@ $html = $html . $stuff; out(" "); out(""); -print($html); +open(OUT, "<", "doc/index.html"); +print(OUT $html); +close(OUT); diff --git a/tools/update.sh b/tools/update.sh new file mode 100755 index 0000000..eb2cdd7 --- /dev/null +++ b/tools/update.sh @@ -0,0 +1,10 @@ +#!/bin/sh +# $Id$ +MAKE=make +if which gmake >/dev/null 2>&1; then + MAKE=gmake +fi +./tools/doc.pl +./tools/genoo.pl +./tools/genmsvc.pl +$MAKE format