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.