diff --git a/make-package b/make-package index 5bf541bca26c231313c0343bccda663d665c11e9..8ea5169ee1e034e6142b6ab8d3e3c4f74d0756ff 100755 --- a/make-package +++ b/make-package @@ -1,8 +1,17 @@ -#!/bin/bash +#!/bin/sh 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" ] ||\ + [ $OS == "NetBSD" ] || [ $OS == "DragonFly" ]; then + MAKE="gmake" +fi + PROJECT="$1" shift @@ -26,7 +35,7 @@ grep -E "^$PROJECT/" _CoqProject >> "$COQFILE" "${COQBIN}coq_makefile" -f "$COQFILE" -o "$MAKEFILE" # Run build -make -f "$MAKEFILE" "$@" +$MAKE -f "$MAKEFILE" "$@" # Cleanup rm -f ".$MAKEFILE.d" "$MAKEFILE"*