3559

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