html_min was phony, so every make deleted output/html_min and minified
all of html/ again, even with nothing changed. A stamp file now stands for
the minified copy and depends on the sources and on minify.py. A list of
the source names, rewritten only when it changes, is a dependency too, so
adding or removing a file in html/ still redoes the copy and a removed
file does not stay behind in the image. If output/html_min is missing,
the stamp is remade in the same run.
The note on version.h in webui-compression.md still said it was phony.