Issue816

Title docs: Use sections in wiki documentation to group similar plugins
Priority feature Status chatting
Superseder Nosy List gabi, jendrik, malte, silvan
Assigned To Keywords
Optional summary
Sub-issues:
* group potential heuristics (issue885)

Created on 2018-09-12.14:41:20 by gabi, last changed by jendrik.

Summary
Sub-issues:
* group potential heuristics (issue885)
Messages
msg8417 (view) Author: jendrik Date: 2018-12-23.12:40:06
Cross-reference issue885.
msg7401 (view) Author: gabi Date: 2018-09-12.14:41:20
In issue749 we introduced the possibility to use sections in the wiki
documentation pages to group similar plugins. So far, this has only been used
for grouping together all PDB heuristics. In this issue, we want to check what
other plugins can be grouped (and do so).

In issue749 Malte made the following comment, which might be useful in this
endeavor:

"The explicit sections would also make it easier to add additional functionality
like section descriptions, explicitly influencing the order in which sections
appear, or documentation pages that speak about several different plug-in types
that are related. (Silvan thought of merge strategies and shrink strategies.)"
History
Date User Action Args
2018-12-23 12:40:06jendriksetstatus: unread -> chatting
messages: + msg8417
summary: Sub-issues: * group potential heuristics (issue885)
2018-09-12 14:51:30silvansetnosy: + silvan
2018-09-12 14:48:44jendriksettitle: docs: Use sections in wiki documentation to group similar plugin -> docs: Use sections in wiki documentation to group similar plugins
2018-09-12 14:48:24jendriksetnosy: + malte, jendrik
2018-09-12 14:41:20gabicreate