diff -r 31d1807b55d8 -r 25921fa4d40f check_release.pl
--- a/check_release.pl	Tue Oct 04 14:45:36 2011 +0200
+++ b/check_release.pl	Thu May 30 10:17:43 2013 +0200
@@ -80,10 +80,6 @@
     }
     close(CR);
 
-    if ((length $current_release == 3) && ($current_release =~ /0$/)) {
-        $current_release = "$current_release.0";
-    }
-
     return $current_release;
 }