diff options
-rwxr-xr-x | update_html | 13 |
1 files changed, 11 insertions, 2 deletions
diff --git a/update_html b/update_html index b33ca08d..5ca4d74b 100755 --- a/update_html +++ b/update_html @@ -1,8 +1,6 @@ #!/bin/bash # Regenerate html files. -rm html/*.html html/edit/*.html - process() { vim -c TOhtml -c write -c qall $1 @@ -22,6 +20,17 @@ process() { mv -i $1.html html/`dirname $1` } +if [ $# -gt 0 ] +then + for f in $* + do + process $f + done + exit 0 +fi + +rm html/*.html html/edit/*.html + for f in *.cc *.mu edit/*.mu do process $f |