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/3702/head
parent
b433c209b3
commit
17376dd284
Loading…
Reference in new issue