19 Apr
2023
19 Apr
'23
4:43 p.m.
- Presumably the user intentionally added the "unroll" attribute, so they may want to know that we're ignoring it. It's one thing to ignore a particular attribute, but quite another to do so silently.
On those grounds I suppose we could add a fixme whose severity is warning rather than error.