aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
-rw-r--r--Makefile2
1 files changed, 1 insertions, 1 deletions
diff --git a/Makefile b/Makefile
index de9da384..aabd01a4 100644
--- a/Makefile
+++ b/Makefile
@@ -278,7 +278,7 @@ latexdoc:
# (currently: export extra Coq-functions for OCaml code, depending on the target)
extraction/extraction.v: Makefile extraction/extraction.vexpand
(echo "(* WARNING: this file is generated from extraction.vexpand *)"; \
- echo "(* by the Makefile -- target \"extraction/extraction.v\" *)\n"; \
+ echo "(* by the Makefile -- target \"extraction/extraction.v\" *)"; \
cat extraction/extraction.vexpand; \
echo "$(EXTRA_EXTRACTION)"; \
echo ".") > extraction/extraction.v