build: minify the web files only when they change

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.

doc/webui-compression.md

@@ -79,8 +79,11 @@ JSON polling of the visible section).
   computation no longer depends on uninitialised buffer content.
 - `version.h` is now written by a single atomic `printf` (change from
   upstream) instead of five separate `echo`s, so a parallel build
-  (`make -j`) can no longer read a half-written copy.  It stays in
-  `.PHONY` so it is regenerated on every build.
+  (`make -j`) can no longer read a half-written copy.  It depends on
+  `FORCE`, so its recipe runs on every build, but the file is only
+  rewritten when its content changes.  The minified copy in
+  `output/html_min/` is redone only when a web file, the list of web
+  files or `tools/minify.py` changes.
 
 ## Verification