Closed FeldrinH closed 2 months ago
Thanks for pointing this out, but it is undocumented on purpose. The explodeGroupWarnings
is a "secret" configuration for our internal use only and we do not want to "advertise" it outside because it is not in a state of showing stuff in the right way, yet.
You can read more about it in #44 and #45.
In that case I propose reopening https://github.com/goblint/GobPie/issues/44 since the feature is not complete.
EDIT: Or opening a new issue to track the finalization of explodedGroupWarnings: false
functionality.
GobPieConfiguration
includes anexplodeGroupWarnings
field, but it is not documented in the readme.