fix getdistro for debians as wheezy has gone from 7.0 to 7.1
authorThierry Parmentelat <thierry.parmentelat@inria.fr>
Wed, 26 Jun 2013 06:54:41 +0000 (08:54 +0200)
committerThierry Parmentelat <thierry.parmentelat@inria.fr>
Wed, 26 Jun 2013 06:54:41 +0000 (08:54 +0200)
build.common

index 5d49603..53371c0 100644 (file)
@@ -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