Add text size
- general text size option
- UI: Modify text size buttons [+] et [-]
Solution 1
- patch text size globally
Solution 2
- add a new portal parameter: TextSize
- add new widgets in the UI
(from redmine: issue id 2906, created on 2020/10/06 by Serge Heiden)