diff options
| author |  pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-05-25 12:50:13 +0000 |
|---|---|---|
| committer | pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-05-25 12:50:13 +0000 |
| commit | bdeccec95e1d018ffb18af9209060a9806d0235a (patch) | |
| tree | fcc156e3b6ed411cbae70f06e082f07b0b55f4fe /tools/coq_makefile.ml | |
| parent | 83e8538118c0b060cb6f231726cda9178f4146bc (diff) | |
Bugs revealed by playing with contribs
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15364 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tools/coq_makefile.ml')
| -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 b9113c08e..5105ac6c9 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 |