Private record fields

Description

I'm wondering if we could change record extension ("redef record XXX +=" …) so that the new fields are only publicly visible if the extension is part of an export section; if not, only the defining namespace would be able to access them.

Environment

None

Assignee

Unassigned

Reporter

Robin Sommer

Labels

None

External issue ID

1003

Components

Affects versions

Priority

Low
Configure