Changeset 3996

Timestamp:

10/09/08 13:04:48 (1 month ago)

Author:

larsivi

Message:

Fix for bash, thanks Cyborg16, refs #1302

Files:

trunk/lib/build-gdc.sh

r3644	r3996
63	63	then
64	64	MAKE=`which make`
65		if [ ! ~~`$MAKE --version \| grep 'GNU Make'`~~ ]
	65	if [ ! "`$MAKE --version \| grep 'GNU Make'`" ]
66	66	then
67	67	echo 'No supported build tool found.'