Added proper deallocation of history buffer

diff --git a/kernel/driver.cc b/kernel/driver.cc
index 0bb12f94ddc4eb45092613dd7bed97c6c8bef9aa..8765c8b871233e81da34820a551c3fd2ed09b032 100644 (file)
--- a/kernel/driver.cc
+++ b/kernel/driver.cc
@@ -617,6 +617,11 @@ int main(int argc, char **argv)
                        write_history(history_file.c_str());
        }
 
+       clear_history();
+       HIST_ENTRY **hist_list = history_list();
+       if (hist_list != NULL)
+               free(hist_list);
+
        for (auto f : log_files)
                if (f != stderr)
                        fclose(f);