The wiki pages were copies of doc/html made by a script run by hand outside
this repository, so the wiki drifted from master whenever that step was
skipped.
Copy them from a workflow instead, taking master as the source and committing
only when a page actually changed.
GitHub wikis cannot run Actions, so the workflow lives here and pushes to the
wiki repository rather than the other way round.
It runs on a push touching doc/html, and also after the documentation workflow
finishes: that workflow commits with GITHUB_TOKEN, and GitHub does not raise
push events for those commits, so a push trigger alone would never see
regenerated HTML.
