aboutsummaryrefslogtreecommitdiff
path: root/coqprime/Makefile
diff options
context:
space:
mode:
Diffstat (limited to 'coqprime/Makefile')
-rw-r--r--coqprime/Makefile5
1 files changed, 2 insertions, 3 deletions
diff --git a/coqprime/Makefile b/coqprime/Makefile
index c8e44a658..2b995982e 100644
--- a/coqprime/Makefile
+++ b/coqprime/Makefile
@@ -14,7 +14,7 @@
#
# This Makefile was generated by the command line :
-# coq_makefile -f _CoqProject -o Makefile
+# coq_makefile -f _CoqProject -o Makefile
#
.DEFAULT_GOAL := all
@@ -151,7 +151,7 @@ endif
# #
#######################################
-all: $(VOFILES)
+all: $(VOFILES)
quick: $(VOFILES:.vo=.vio)
@@ -316,4 +316,3 @@ $(addsuffix .beautified,$(VFILES)): %.v.beautified:
# Edit at your own risks !
#
# END OF WARNING
-