Albert S 10d61acbd0 shared,gui: SearchResult: remove page vector
Since the previous commit we don't group the results
anymore, making the vector redundant
2022-08-24 00:00:11 +02:00
..
2022-02-27 23:10:46 +01:00
2022-02-27 23:10:46 +01:00
2022-06-21 22:33:50 +02:00