From dfd812884d68c18e0ec20dba849af485ac928010 Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Mon, 18 Dec 2023 12:16:00 +0100
Subject: [PATCH] vector: fix missing destructor call

---
 src/util/vector.h | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/src/util/vector.h b/src/util/vector.h
index 43a4e8921..d684f43eb 100644
--- a/src/util/vector.h
+++ b/src/util/vector.h
@@ -559,8 +559,7 @@ public:
         for(; pos != e; ++pos, ++prev) {
             *prev = std::move(*pos);
         }
-        reinterpret_cast<SZ *>(m_data)[SIZE_IDX]--;
-        // TODO: where is the destructor called?
+        pop_back();
     }
 
     void erase(T const & elem) {