fix(util/buffer): destructor was not being invoked at erase and erase_elem

This bug was producing a weird memory leak in the definition package.
The methods erase and erase_elem are not used very often. This is why
this bug was never detected.
This commit is contained in:
Leonardo de Moura 2015-01-27 18:48:02 -08:00
parent 94519b48b1
commit 1119a8018a

View file

@ -151,7 +151,7 @@ public:
lean_assert(idx < size());
for (unsigned i = idx+1; i < size(); i++)
m_buffer[i-1] = m_buffer[i];
m_pos--;
pop_back();
}
void erase_elem(T const & elem) {