Vladimir Dubrovin f599c3239c Publish documentation to the wiki when the HTML changes ... 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.		2026-08-22 14:42:59 +03:00
..
workflows	Publish documentation to the wiki when the HTML changes	2026-08-22 14:42:59 +03:00
dependabot.yml	Add more docker platforms	2026-06-01 20:16:19 +03:00