This was necessary for hooking display.refresh() with the old UI toolkit. With the new one, we explicitly refresh the display after every paint, so implicit after-step refresh seems no longer necessary.pull/3633/head
parent
da536b81ae
commit
0dd113b898
Loading…
Reference in new issue