Closed this issue 4 years ago · 0 comments
CC @njlbenn See details of workaround that needs to be removed as soon as Dotty issue #9688 is resolved
See comment for details.
Note that this workaround is applied in 4 places in the code.