From eaa70347742788afe935bafc6be28e7b0c0bd2cf Mon Sep 17 00:00:00 2001
From: Gabriel Corona <gabriel.corona@loria.fr>
Date: Thu, 9 Jun 2016 11:57:03 +0200
Subject: [PATCH] [jenkins] Add lib/ in the PATH for Windows

---
 tools/jenkins/build.sh | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/tools/jenkins/build.sh b/tools/jenkins/build.sh
index 7a77cf8d41..1421468644 100755
--- a/tools/jenkins/build.sh
+++ b/tools/jenkins/build.sh
@@ -88,6 +88,9 @@ fi
 mkdir $WORKSPACE/build
 cd $WORKSPACE/build
 
+# This is for Windows:
+PATH="$WORKSPACE/build/lib:$PATH"
+
 if test "$(uname -o)" != "Msys"; then
   echo "XX"
   echo "XX Build the archive out of the tree"
-- 
2.20.1