Closed this issue 5 years ago · 1 comments
It is only used for error reporting, kind of clumsily. Update the message in error reporting accordingly.
Resolved by #378.