35 lines
1.1 KiB
Markdown
35 lines
1.1 KiB
Markdown
# 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.
|