From 79b7f7a89ad565a17012ee12c9774c1bd9fa508c Mon Sep 17 00:00:00 2001
From: Arnaud Giersch <arnaud.giersch@univ-fcomte.fr>
Date: Thu, 16 May 2019 15:58:53 +0200
Subject: [PATCH] Correctly split os/ver on redhat-like.

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

diff --git a/tools/jenkins/build.sh b/tools/jenkins/build.sh
index 0e66fd62a1..72a3f5709f 100755
--- a/tools/jenkins/build.sh
+++ b/tools/jenkins/build.sh
@@ -72,8 +72,7 @@ elif [ -f /etc/debian_version ]; then
     os=Debian
     ver=$(cat /etc/debian_version)
 elif [ -f /etc/redhat-release ]; then
-    os=""
-    ver=$(cat /etc/redhat-release)
+    read -r os ver < /etc/redhat-release
 elif [ -f /usr/bin/sw_vers ]; then
     os=$(sw_vers -productName)
     ver=$(sw_vers -productVersion)
-- 
2.20.1