[vector] Merge sorted-vector into vector Was easier than I thought! Let's see what the bot gods think...
2022-01-19T11:38:37