TEC 975599e822 More CI fiddling ... 1. Run CI more to get around branch deletion Because my Gitea source repo deletes the CI-generated branch when it syncs to GitHub. 2. Deploy directly to GH pages This avoids the problem with gh-pages disabling when the branch is deleted. 3. A few other little tweaks		2023-01-24 18:21:51 +08:00
..
workflows	More CI fiddling	2023-01-24 18:21:51 +08:00
FUNDING.yml	Give people a way to caffeinate me	2021-08-24 17:54:16 +08:00