diff --git a/make-package b/make-package index 2c55199cea889001198ecb1327699f1bb06a97d4..8ea5169ee1e034e6142b6ab8d3e3c4f74d0756ff 100755 --- a/make-package +++ b/make-package @@ -3,6 +3,8 @@ set -e # Helper script to build and/or install just one package out of this repository. # Assumes that all the other packages it depends on have been installed already! +# Make sure we get a GNU version of make. +# This is exactly how opam determines which make executable to use. OS=$(uname) MAKE="make" if [ $OS == "FreeBSD" ] || [ $OS == "OpenBSD" ] ||\