Index: tools/check.sh
===================================================================
--- tools/check.sh	(revision a9a6d8d95fe03e64b79524407f435fc49903fa54)
+++ tools/check.sh	(revision a1d7b4b64d80fd99178eff41903b8d4810473657)
@@ -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