Mon, 10 Aug 2020 13:58:55 +0200SVGHMI: provide request_animate() to Widget authors so that they can register redraw code when events lead to redraw. Widget member animate() is called when it is time to update DOM. svghmi
Edouard Tisserant [Mon, 10 Aug 2020 13:58:55 +0200] rev 3019
SVGHMI: provide request_animate() to Widget authors so that they can register redraw code when events lead to redraw. Widget member animate() is called when it is time to update DOM.

Mon, 10 Aug 2020 11:30:06 +0200Merge svghmi
Edouard Tisserant [Mon, 10 Aug 2020 11:30:06 +0200] rev 3018
Merge