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