1#!/bin/sh 2#*---------------------------------------------------------------------*/ 3#* flags */ 4#*---------------------------------------------------------------------*/ 5make=make 6 7#*---------------------------------------------------------------------*/ 8#* We parse the arguments */ 9#*---------------------------------------------------------------------*/ 10while : ; do 11 case $1 in 12 "") 13 break;; 14 15 --make=*) 16 make="`echo $1 | sed 's/^[-a-z]*=//'`";; 17 18 -*) 19 echo "Unknown option \"$1\", ignored" >&2;; 20 esac 21 shift 22done 23 24# Check the make version number 25$make -v --version | grep -i "gnu make" > /dev/null 26 27# Return the grep result 28exit $? 29