[PATCH] Detect correct make command in configure

[Richard Guenther]

Hi!

On debian, GNU make is installed as make while gmake is not available.
So setting $make to gmake in configure fails to create the suite
directories and thus the build fails.

Ok?

Richard.

2002Jan09  Richard Guenther <richard.guenther at uni-tuebingen.de>

	* configure: use make, if gmake is not available.

diff -u -u -r1.106 configure
--- configure	6 Jan 2003 17:49:58 -0000	1.106
+++ configure	8 Jan 2003 23:04:27 -0000
@@ -100,8 +100,15 @@
 #
 ###########################################################################

-### the name of the make program
-$makecmd         = gmake;
+### the name of the make program - gmake if available, else make
+if ( system("gmake README") == 0 )
+  {
+     $makecmd         = gmake;
+  }
+else
+  {
+     $makecmd         = make;
+  }

 ### the directory of the config and arch files, and the archfile extension
 $configsuitedir  = "config";