Do we need this PR at all? It seems the requested changes are also handled in #1242.
I must have applied due to using two computers.
—
Reply to this email directly, view it on GitHub, or unsubscribe.
You are receiving this because you are subscribed to this thread.