--- GPI2-1.2.0/src/GPI2_Utility.h.orig	2015-05-13 17:42:36.000000000 +0200
+++ GPI2-1.2.0/src/GPI2_Utility.h	2015-06-16 21:56:09.572397490 +0200
@@ -25,7 +25,6 @@
 #include <stdlib.h>
 #include <stdio.h>
 #include <time.h>
-#include <xmmintrin.h>
 
 #ifdef DEBUG
 #include "GPI2.h"
@@ -56,7 +55,12 @@
 #ifdef MIC
 #define gaspi_delay() _mm_delay_32(32)
 #else
-#define gaspi_delay() _mm_pause()
+#if defined(__i386__) || defined(__x86_64__)
+#define gaspi_delay()   __builtin_ia32_pause()
+#else
+#include <unistd.h>
+#define gaspi_delay()   usleep(0)
+#endif
 #endif