1.1 KiB
PR#100: The docs category of werkregie is doc/
WARNING: This document describes only the change applied in this PR. It may already be outdated once the next PR is merged. Historic PR documentation is not maintained along with new PRs; treat it as a snapshot.
Problem
werkregie keeps its documentation in doc/, but config/werkregie.toml names docs/** as the docs category.
So doc/werkregie.werkbaum counts as other:
Jev judges it like code, the size limits count it, and the model gets it in full.
Non-Goals
- No change of the docs category of another repository.
Solution
[categories] docs of werkregie is ["**/*.md", "doc/**"], since werkregie keeps its documentation in doc/.
The machine config of werkregie on mih09 gets the changed host config.
A new test checks for werkrevisor, werkator, werkcrappit and werkregie that their plan counts as documentation; it fails for werkregie without the fix.
The header of config/werkregie.toml says that a PR of werkregie never changes the file;
"the PR" read like any PR, also this one.
Open Questions
None.
Follow-up PRs
None.