--- scripts/Makefile.in.orig	2014-02-03 10:37:08.000000000 +0100
+++ scripts/Makefile.in	2014-02-03 10:38:36.000000000 +0100
@@ -562,7 +562,7 @@
 	@(diff scripts-listed-in-makefile.txt contents-of-tree.txt; \
 	  rm -f scripts-listed-in-makefile.txt contents-of-tree.txt; \
 	  RV=$$?; \
-	  if [[ $$RV == 0 ]] ; \
+	  if [ $$RV = 0 ] ; \
 	      then echo " ... ok"; \
 	  else \
 	      false; \