On Tuesday, 16 June 2020 at 10:44:46 UTC, Dukc wrote: > Bump (we don't want to forget a DIP discussion now do we?) Seems the feature is not controversal - nobody complains, so it seems everybody is pleased with it. Let's move it forward!