Jean-Marc Lasgouttes
58d22e0c6e
Keep last file positions in last-use ordering
...
Using a map would sort the elements in alphabetic ordering, which
means that when the number of elements is larger than 100, the wrong
elements get pruned.
This commit uses a list instead. Searching an item needs linear time,
but this should not be a problem for a list with less than 100
elements.
Fixes bug #10310 .
2019-10-20 12:37:27 +02:00
..
2019-04-19 14:46:12 +02:00
2018-09-21 21:46:47 +02:00
2019-10-07 15:31:30 +02:00
2018-12-29 19:14:41 +00:00
2019-09-17 23:15:09 +02:00
2019-09-28 16:08:06 +02:00
2019-09-16 00:03:56 +02:00
2019-04-26 16:55:30 +02:00
2019-08-14 17:07:47 +02:00
2017-07-30 09:30:58 +02:00
2017-07-30 00:54:12 +02:00
2017-07-03 13:53:14 -04:00
2019-09-13 11:49:29 -04:00
2019-09-13 11:49:29 -04:00
2017-07-23 13:11:54 +02:00
2018-08-14 17:05:40 +02:00
2019-09-13 16:23:49 +02:00
2019-06-07 16:47:04 +02:00
2018-04-28 13:31:29 +02:00
2019-02-25 15:19:58 +01:00
2019-02-25 15:19:58 +01:00
2019-09-13 16:23:49 +02:00
2019-09-13 16:23:49 +02:00
2019-10-20 12:37:27 +02:00
2019-07-19 11:52:03 +02:00
2018-12-06 10:30:58 +01:00
2018-02-18 09:19:03 +01:00
2019-08-07 13:00:29 +02:00
2017-07-23 13:11:54 +02:00
2018-02-23 23:17:57 -05:00
2017-10-03 22:12:23 +02:00
2018-02-23 23:38:31 -05:00
2017-07-03 13:46:30 -04:00
2017-10-16 10:12:21 +02:00
2017-10-16 10:12:21 +02:00
2017-07-03 13:46:30 -04:00
2017-10-16 15:48:47 -04:00
2017-07-03 13:46:30 -04:00
2019-06-07 16:47:04 +02:00
2018-04-16 14:02:20 -04:00
2017-07-23 13:11:54 +02:00
2018-09-18 23:07:48 +02:00
2018-09-18 23:07:48 +02:00
2019-07-20 12:57:16 +02:00
2019-07-19 11:52:03 +02:00
2017-07-05 14:46:34 +02:00
2017-07-03 13:46:30 -04:00
2019-09-11 22:13:25 -04:00
2018-07-22 23:20:21 +02:00
2017-03-13 17:06:42 +01:00
2017-03-20 15:38:08 +01:00
2018-12-17 15:33:47 +01:00
2017-07-03 13:46:30 -04:00
2019-04-18 15:27:24 +02:00
2019-01-04 13:55:57 +01:00
2017-07-23 13:11:54 +02:00
2018-01-30 12:11:22 +01:00
2019-06-17 16:19:31 +02:00
2019-03-19 22:46:33 +01:00
2017-03-01 16:34:01 +01:00
2018-02-24 00:30:24 -05:00
2019-08-12 12:18:28 +02:00
2019-08-12 12:18:28 +02:00
2019-08-21 12:33:13 +02:00
2019-05-10 10:45:40 +02:00
2019-06-14 17:05:49 +02:00
2019-06-14 17:05:49 +02:00
2019-05-10 10:45:40 +02:00
2017-07-03 13:53:14 -04:00
2018-12-14 11:41:16 +01:00
2019-09-11 10:29:50 +02:00
2019-07-22 15:20:38 +02:00
2018-04-20 23:37:58 -04:00
2018-04-21 23:05:21 -04:00
2017-07-03 13:53:14 -04:00
2017-07-03 13:46:30 -04:00
2018-03-29 18:43:11 +02:00
2018-02-23 23:47:05 -05:00
2017-07-03 13:46:30 -04:00
2018-05-28 12:33:17 +02:00
2018-05-28 12:33:17 +02:00
2019-03-09 12:00:40 +01:00
2019-03-09 12:00:40 +01:00
2019-03-09 12:00:40 +01:00
2019-03-09 12:00:40 +01:00
2019-08-14 13:10:42 +02:00
2019-08-14 13:10:42 +02:00
2019-09-10 10:43:40 -04:00
2019-06-07 16:47:04 +02:00
2019-08-15 15:15:59 +02:00
2019-09-13 16:23:49 +02:00
2019-09-13 16:23:49 +02:00
2019-09-13 16:23:49 +02:00
2019-06-02 18:07:10 +02:00
2019-06-02 18:07:10 +02:00
2017-07-03 13:53:14 -04:00
2017-07-03 13:46:30 -04:00
2017-07-03 13:53:14 -04:00
2018-01-28 23:37:20 -05:00
2018-01-05 20:14:04 +01:00
2018-01-05 20:14:04 +01:00
2017-07-23 13:11:54 +02:00
2017-08-29 15:30:44 +02:00
2017-07-03 13:46:30 -04:00
2019-03-19 07:13:18 +01:00
2017-03-13 23:40:29 -04:00
2019-07-22 15:20:38 +02:00
2018-08-18 16:11:08 +02:00
2019-09-13 16:23:49 +02:00
2019-09-13 16:23:49 +02:00
2019-09-11 10:29:50 +02:00
2019-07-22 08:05:28 +02:00
2017-07-03 13:53:14 -04:00
2019-07-28 22:01:17 +02:00
2017-04-12 21:19:42 +02:00
2019-07-20 23:39:40 +02:00
2019-07-15 13:38:07 +02:00
2019-07-15 13:38:07 +02:00
2019-04-20 09:28:46 +02:00
2019-05-14 16:39:35 +02:00
2017-07-03 13:46:30 -04:00
2017-07-23 13:11:54 +02:00
2019-10-07 15:31:10 +02:00
2018-05-01 14:21:05 +02:00
2018-07-15 14:26:29 +02:00
2017-10-16 21:28:44 -04:00
2019-09-13 16:23:49 +02:00
2017-07-23 13:11:54 +02:00
2019-07-11 10:31:10 +02:00
2019-08-14 13:10:42 +02:00
2019-08-16 11:48:57 +02:00
2019-07-10 14:50:08 +02:00
2017-11-11 13:24:08 +01:00
2017-11-11 13:24:08 +01:00
2017-07-03 13:46:30 -04:00
2019-05-07 16:16:35 +02:00
2019-09-13 19:01:26 +02:00
2017-07-03 13:53:14 -04:00
2019-06-05 15:50:53 +02:00
2019-05-23 10:26:08 +02:00
2019-05-23 11:30:35 +02:00
2018-09-20 11:58:08 +02:00
2018-08-07 17:56:07 +02:00
2017-06-11 19:51:17 +02:00
2019-10-20 12:37:27 +02:00
2019-10-20 12:37:27 +02:00
2017-12-23 13:27:10 +01:00
2017-12-23 13:27:10 +01:00
2017-07-03 13:46:30 -04:00
2019-06-12 15:03:18 +02:00
2019-03-21 14:18:17 +01:00
2018-12-06 10:30:58 +01:00
2019-09-13 16:23:49 +02:00
2019-09-11 22:13:58 -04:00
2019-09-11 19:39:03 -04:00
2019-09-13 16:23:49 +02:00
2019-08-12 12:18:28 +02:00
2019-08-07 16:44:11 +02:00
2019-07-14 23:27:44 +02:00
2019-03-12 16:03:22 +01:00
2017-07-23 13:11:54 +02:00
2019-09-13 16:23:49 +02:00
2019-09-13 16:23:49 +02:00
2018-02-24 00:28:37 -05:00
2019-09-13 16:23:49 +02:00
2019-06-02 21:17:26 +02:00
2018-05-02 12:38:40 +02:00
2019-07-28 22:01:17 +02:00
2019-07-28 22:01:17 +02:00
2019-08-14 16:55:43 +02:00
2017-07-03 13:53:14 -04:00
2017-07-03 13:53:14 -04:00