Index: tools/check.sh
===================================================================
--- tools/check.sh	(revision a9a6d8d95fe03e64b79524407f435fc49903fa54)
+++ tools/check.sh	(revision b6913b7a680d8a82aa53cc8eaf2b9a5df83eac1a)
@@ -66,5 +66,5 @@
 do
 	echo -n ">>>> Building $P... "
-	( make distclean && make PROFILE=$P HANDS_OFF=y $1 ) >>/dev/null 2>>/dev/null
+	( make distclean && make PROFILE=$P HANDS_OFF=y "$@" ) >>/dev/null 2>>/dev/null
 	if [ $? -ne 0 ];
 	then