diff options
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/coq_makefile.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index b9113c08e3..5105ac6c90 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -201,7 +201,7 @@ let install_doc some_vfiles some_mlifiles (_,inc_r) = if some_mlifiles then install_one_kind "mlihtml" rt; end else begin prerr_string "Warning: -R options don't have a correct common prefix, - install-doc will put anything in $INSTALLDEFAULTROOT"; + install-doc will put anything in $INSTALLDEFAULTROOT\n"; if some_vfiles then install_one_kind "html" "$(INSTALLDEFAULTROOT)"; if some_mlifiles then install_one_kind "mlihtml" "$(INSTALLDEFAULTROOT)"; end in |