bot icon indicating copy to clipboard operation
bot copied to clipboard

Make documentation of coqbot autominimization more discoverable

Open JasonGross opened this issue 2 years ago • 0 comments

@JasonGross The documentation of this feature, currently located at https://github.com/coq/coq/wiki/Coqbot-minimize-feature, should probably be updated.

BTW, I don't think that the current location for the documentation of this feature is good, because it's hardly discoverable. Probably, it should be a specific file in the bot repo, that would be linked from both the bot README and the contributing guide of Coq (currently, this section https://github.com/coq/coq/blob/master/CONTRIBUTING.md#reporting-a-bug-requesting-an-enhancement references the find-bug.py utility but not the coqbot feature).

Originally posted by @Zimmi48 in https://github.com/coq/bot/issues/256#issuecomment-1404788951

JasonGross avatar Jan 26 '23 17:01 JasonGross