Use gmake for BSD systems

This PR modifies the make-package script so it runs on systems whose default make executable is BSD Make rather than GNU Make. It checks the os type and decides whether to run gmake or make. This is exactly how opam determines which make executable to use.

I also changed the script to use sh instead of bash because make-package doesn't seem to depend on bash-specific features and sh has a more standard path.

added 1 commit

• c5e98d55 - Apply 1 suggestion(s) to 1 file(s)

Compare with previous version

resolved all threads

Thanks for the MR!

mentioned in commit f2a1f915

merged

I have added this to the changelog as well.

@yiyunliu any chance you could make the same PR for https://gitlab.mpi-sws.org/iris/iris/ ? :)

Done! iris!1061 (merged)

I added your comments to the make-package file but didn't modify the changelog because I'm not sure if I'm supposed to.

mentioned in merge request iris!1061 (merged)