← Back to branch summary

~martin-decky/helenos/rcu

« back to all changes in this revision

Viewing changes to tools/check.sh

  • Committer: Vojtech Horky
  • Date: 2012-04-01 18:44:23 UTC
  • mfrom: (1443.1.3 misc)
  • Revision ID: vojtechhorky@users.sourceforge.net-20120401184423-vb1p25ijzfnrx6so
Merge improvemens from GSOC12 "how-do-you-do period"

Show diffs side-by-side

added added

removed removed

Lines of Context:
tools/check.sh
65
65
for P in $PROFILES;
66
66
do
67
67
        echo -n ">>>> Building $P... "
68
 
        ( make distclean && make PROFILE=$P HANDS_OFF=y $1 ) >>/dev/null 2>>/dev/null
 
68
        ( make distclean && make PROFILE=$P HANDS_OFF=y "$@" ) >>/dev/null 2>>/dev/null
69
69
        if [ $? -ne 0 ];
70
70
        then
71
71
                FAILED="$FAILED $P"