diff options
Diffstat (limited to 'tools')
-rwxr-xr-x | tools/update_html | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/tools/update_html b/tools/update_html index c5589418..0f073377 100755 --- a/tools/update_html +++ b/tools/update_html @@ -8,6 +8,7 @@ set -e # generate html/$1.html using /tmp/tags process() { + mkdir -p html/`dirname $1` rm -f html/$1.html convert_html $1 tools/linkify /tmp/tags html/$1.html @@ -70,4 +71,14 @@ do process $f done +for f in apps/*/*.mu +do + test $# -gt 0 && test $1 != $f && continue + echo $f + ( cd `dirname $f` + ctags -x ../../[0-9]*.subx ../../[0-9]*.mu `basename $f` > /tmp/tags + ) + process $f +done + rm /tmp/tags |