diff --git a/tools/README.txt b/tools/README.txt index 55140d7fad..44b0427427 100644 --- a/tools/README.txt +++ b/tools/README.txt @@ -135,6 +135,12 @@ mkexport.sh and Makefile.export Makefile.export is used only by the mkexport.sh script to parse out options from the top-level Make.defs file. + USAGE: tools/mkexport.sh [-d] [-z] [-u] [-w|wy|wn] -t [-x ] -l "lib1 [lib2 [lib3 ...]]" + + Thais script also depends on the environment variable MAKE which is set + in the top-level Makefile before starting mkexport.sh. If MAKE is not + defined, the script will set it to `which make`. + mkfsdata.pl ----------- diff --git a/tools/mkexport.sh b/tools/mkexport.sh index ebaff91b88..348a14cf5c 100755 --- a/tools/mkexport.sh +++ b/tools/mkexport.sh @@ -1,7 +1,7 @@ #!/bin/bash # tools/mkexport.sh # -# Copyright (C) 2011-2012, 2014 Gregory Nutt. All rights reserved. +# Copyright (C) 2011-2012, 2014, 2016 Gregory Nutt. All rights reserved. # Author: Gregory Nutt # # Redistribution and use in source and binary forms, with or without @@ -115,6 +115,12 @@ if [ ! -f "${TOPDIR}/.version" ]; then exit 1 fi +# Check if the make environment variable has been defined + +if [ -z "${MAKE}" ]; then + MAKE=`which make` +fi + # Get the version string source "${TOPDIR}/.version"