From 267058f3b41b77c23fd316f6f654b82116377bf8 Mon Sep 17 00:00:00 2001
From: Thierry Parmentelat <thierry.parmentelat@sophia.inria.fr>
Date: Wed, 28 Apr 2010 07:55:58 +0000
Subject: [PATCH] fix pl_getDistro - was always returning Redhat

---
 build.common | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/build.common b/build.common
index e179c1bc..390b6f34 100644
--- a/build.common
+++ b/build.common
@@ -18,9 +18,7 @@ export PATH=.:$PATH
 function pl_getDistro() {
     if [ -f "/etc/redhat-release" ] ; then
 	distro=$(awk ' { print $1 } ' /etc/redhat-release)
-	if [ $distro="Red" ] ; then
-		distro="Redhat"
-	fi
+	case $distro in Red*) distro="Redhat" ; esac
     else
 	echo "build.common.pl_getDistro-unknown"
 	exit 1
-- 
2.43.0