From 2ab527e45d44b31125d1befbe7b5e0f225e02ef4 Mon Sep 17 00:00:00 2001
From: Thierry Parmentelat <thierry.parmentelat@inria.fr>
Date: Wed, 26 Jun 2013 08:54:41 +0200
Subject: [PATCH] fix getdistro for debians as wheezy has gone from 7.0 to 7.1

---
 build.common | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/build.common b/build.common
index 5d496032..53371c02 100644
--- a/build.common
+++ b/build.common
@@ -22,8 +22,8 @@ function pl_getDistro() {
 	echo $DISTRIB_CODENAME 
     elif [ -f /etc/debian_version ] ; then
 	case $(cat /etc/debian_version) in
-	    6.0.6) distro=squeeze ;;
-	    7.0)   distro=wheezy  ;;
+	    6.*) distro=squeeze ;;
+	    7.*)   distro=wheezy  ;;
 	    *)	   distro=unknown.debian.in.build.common ;;
 	esac
     fi
-- 
2.47.0