From 99811a9ef366628d1a29e4fb4b50726b3750fb76 Mon Sep 17 00:00:00 2001 From: James Mitchell Date: Thu, 14 Sep 2023 10:02:55 +0100 Subject: [PATCH] Update Makefile Co-authored-by: Max Horn --- Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Makefile b/Makefile index c87ab395d..279e04f56 100644 --- a/Makefile +++ b/Makefile @@ -2,7 +2,7 @@ # This Makefile serves two purposes: # 1) If the user types "make" without having run "configure", we suggest running configure. # 2) Our build system is written for GNU make, and makes liberal use of its features. -# We therefore put it into "GNUmakefile", which is picked up by GNU make, but ignore by +# We therefore put it into "GNUmakefile", which is picked up by GNU make, but ignored by # other make versions, such as BSD make. # Thus, if the user has BSD make, it will run this Makefile instead -- and we inform # them that they need to use GNU make to compile GAP.