--- configure.orig	2014-10-20 01:29:05.836430783 +0200
+++ configure	2014-10-20 01:29:05.872430406 +0200
@@ -9046,10 +9046,11 @@
 			#include <stdio.h>
 			extern unsigned GC_version;
 			int main(void){
-				unsigned min = ((6 << 16) | (4 << 8) | 0);
-				printf("%d.%d.%d ",GC_version >> 16, (GC_version >> 8) & 0xFF, GC_version & 0xFF);
-				if (GC_version>=min) return 0;
-				return 1;
+				printf("%d.%d.%d ", GC_VERSION_MAJOR, GC_VERSION_MINOR, GC_VERSION_MICRO);
+				if (GC_VERSION_MAJOR >= 6 && GC_VERSION_MINOR >= 4)
+				  return 0;
+				else
+				  return 1;
 			}
 _ACEOF
 if ac_fn_cxx_try_run "$LINENO"; then :