aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--Makefile2
1 files changed, 2 insertions, 0 deletions
diff --git a/Makefile b/Makefile
index de4b33edbc..5317bb1d02 100644
--- a/Makefile
+++ b/Makefile
@@ -2,6 +2,8 @@
###########################################################################
# Makefile for Coq
#
+# To be used with GNU Make.
+#
# This is the only Makefile. You won't find Makefiles in sub-directories
# and this is done on purpose. If you are not yet convinced of the advantages
# of a single Makefile, please read