I think DIV_BY_ZERO can be removed as it's dead.
Closed this issue · 1 comments
hawkinsw commented
I think DIV_BY_ZERO can be removed as it's dead.
Originally posted by @Alan-Jowett in #315 (comment)
Alan-Jowett commented
@hawkinsw I think this is fixed now?