Summary
- merged
- NEWS;
- handle font-size events;
- clarified GUI representation of replacement texts with zero or more abbrevs;
- handle update events; tuned;
- discontinued global etc/abbrevs;
- added abbrevs panel;
- tuned;
- more robust;
- maintain abbrevs in canonical reverse order;
- tuned;
- tuned;
- ignore default output directory of 'build_stats' tool