NiLuJe 888d3591b2
Give more control over CRe margins ( #4945 ) ...
Without having to resort to weird custom defaults.
* Split the current margins setting in three:
* Horizontal margins (because you generally want those two to be balanced).
* Top margin & Bottom margin (because you may want to tweak those separately to deal with quirky status bar/final line shenanigans).
* Also, add a "Reclaim bar height from bottom margin" toggle to the status bar menu, to optionally make sure the status bar won't eat into the bottom margin.
* Includes a free fix to diacritics popup refresh handling in the keyboard ;).
2019-05-01 02:09:01 +02:00
2019-03-12 20:00:06 +01:00
2017-09-23 20:24:45 +02:00
2019-03-14 20:58:45 +01:00
2019-03-14 20:58:45 +01:00
2018-01-29 21:27:24 +01:00
2019-04-02 18:27:35 +02:00
2019-05-01 02:09:01 +02:00
2019-03-14 20:58:45 +01:00
2019-02-07 01:14:37 +01:00
2019-03-14 20:58:45 +01:00
2017-10-16 17:51:56 +02:00
2019-05-01 02:09:01 +02:00
2018-01-29 21:27:24 +01:00
2018-02-07 18:45:46 +01:00
2019-02-07 01:14:37 +01:00
2017-05-16 02:11:11 -07:00
2018-10-14 09:14:35 -07:00
2019-03-29 20:12:09 +01:00
2019-02-08 00:56:32 +01:00
2019-03-30 01:30:46 +01:00
2019-04-12 22:46:10 +02:00
2017-08-18 11:43:46 +02:00
2014-03-13 21:52:43 +08:00
2019-03-03 13:10:45 +01:00
2019-01-29 00:05:55 +01:00
2019-04-07 19:00:15 +02:00
2019-03-14 20:58:45 +01:00
2019-04-18 23:26:53 +02:00
2019-03-14 20:58:45 +01:00
2019-02-08 00:56:32 +01:00
2019-04-08 23:05:08 +02:00
2019-03-14 20:58:45 +01:00
2017-04-29 11:41:24 -07:00
2019-03-14 20:58:45 +01:00
2019-03-14 20:58:45 +01:00
2018-08-06 21:16:30 +02:00
2019-03-14 20:58:45 +01:00
2018-04-06 21:13:25 +02:00
2019-02-08 00:56:32 +01:00
2019-02-07 01:14:37 +01:00
2019-03-27 22:50:44 +01:00
2018-06-14 21:53:43 +02:00
2018-04-19 14:24:04 +02:00
2019-04-05 08:50:33 +02:00
2019-03-14 20:58:45 +01:00
2017-08-18 11:43:46 +02:00
2018-08-06 20:59:01 +02:00
2019-03-14 20:58:45 +01:00
2019-03-14 20:58:45 +01:00
2019-02-07 01:14:37 +01:00
2019-03-14 20:58:45 +01:00
2014-03-13 21:52:43 +08:00
2019-02-08 18:31:40 +01:00
2018-08-19 20:21:03 +02:00
2019-03-31 22:00:07 +02:00
2019-02-08 00:56:32 +01:00
2019-01-15 23:56:11 +01:00
2019-03-18 09:35:27 +01:00
2019-02-07 01:14:37 +01:00
2019-03-29 20:12:09 +01:00
2018-02-07 18:45:46 +01:00
2019-03-14 20:58:45 +01:00
2019-03-14 20:58:45 +01:00
2018-01-17 21:36:21 +01:00
2017-08-18 11:43:46 +02:00
2018-08-01 18:33:52 +02:00
2014-03-13 21:52:43 +08:00
2019-05-01 02:09:01 +02:00
2016-12-25 12:13:53 -08:00
888d3591b2