diff options
| author | Jaakko Keränen <jaakko.keranen@iki.fi> | 2020-10-18 08:01:08 +0300 |
|---|---|---|
| committer | Jaakko Keränen <jaakko.keranen@iki.fi> | 2020-10-18 08:01:08 +0300 |
| commit | b31764ed2a12d27053dba8ec7a6780f730d426e5 (patch) | |
| tree | 2db1e94cde259c7fb42ea34d21b010ffa37b9872 /src/ui/playerui.c | |
| parent | 6329646833a719097ef2e7eec42665ab0437d91f (diff) | |
DocumentWidget: Improved audio player UI refresh
There is no need to prioritize animation smoothness when it comes to audio players. Just post timer events at a relaxed 15 Hz when active players are visible.
Fixes an issue on macOS (and possibly other platforms) where moving the window was very glitchy if a player was active.
Diffstat (limited to 'src/ui/playerui.c')
0 files changed, 0 insertions, 0 deletions