3 commits

Author	SHA1	Message	Date
Ilya Grigoriev	f31e66d663	github: rename jj-docs-bot to jj-docs[bot] ... Perhaps this will stop Github from showing jj-docs-bot as a very active contributor in https://github.com/martinvonz/jj/pulse. This would probably fair, even though jj-docs-bot tries its best to be a good and helpful bot. Regardless, this seems to be the standard on Github which has `dependabot[bot]` and `github-actions[bot]`.	2023-09-15 19:31:48 -07:00
dependabot[bot]	d420ca06d0	github: bump the github-dependencies group with 1 update ... Bumps the github-dependencies group with 1 update: [actions/checkout](https://github.com/actions/checkout). - [Release notes](https://github.com/actions/checkout/releases) - [Changelog](https://github.com/actions/checkout/blob/main/CHANGELOG.md) - [Commits](https://github.com/actions/checkout/compare/v3...3df4ab11eba7bda6032a0b82a6bb43b11571feac) --- updated-dependencies: - dependency-name: actions/checkout dependency-type: direct:production update-type: version-update:semver-major dependency-group: github-dependencies ... Signed-off-by: dependabot[bot] <support@github.com>	2023-09-04 13:39:04 -07:00
Ilya Grigoriev	c8bb8fbeb2	Github actions to build docs ... One action publishes the 'prerelease' version on every push to `main`. The other publishes a 'latest' version on every releasse. I tested both of them, but not with branch protection rules.	2023-08-28 10:43:48 -07:00