From 793b2817ec1bb68f880af6f7820cb1388d986d0e Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 29 Jul 2014 10:57:20 -0700
Subject: [PATCH] fix(util/lean_path): clear g_lean_path_vector before
 (re-)initializing it

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/util/lean_path.cpp | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/util/lean_path.cpp b/src/util/lean_path.cpp
index f5b21239b..23a585d11 100644
--- a/src/util/lean_path.cpp
+++ b/src/util/lean_path.cpp
@@ -167,6 +167,7 @@ void init_lean_path(char const * kernel_instance_name) {
     } else {
         g_lean_path = r;
     }
+    g_lean_path_vector.clear();
     g_lean_path = normalize_path(g_lean_path);
     unsigned i  = 0;
     unsigned j  = 0;