From c5e98d5570e127a8aa246e7af9c49fd2249a1794 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 30 Jul 2024 00:06:22 +0000
Subject: [PATCH] Apply 1 suggestion(s) to 1 file(s)

Co-authored-by: Ralf Jung <jung@mpi-sws.org>
---
 make-package | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/make-package b/make-package
index 2c55199c..8ea5169e 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" ] ||\
-- 
GitLab