aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2015-02-26 15:03:36 +0100
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2015-02-26 15:03:36 +0100
commitb4a16a43d9f84969feb7b8b090092260cb898e23 (patch)
treec30fc9ce0e6e9e7eeedd2ee346be6f6ab223add7 /tools
parent15a3b57db10e61c9de12b5880b04b46db1494b5b (diff)
Fixing printing error in coq_makefile.
Diffstat (limited to 'tools')
-rw-r--r--tools/coq_makefile.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index bd78fe2c5..84b4b5e5d 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -158,7 +158,7 @@ let vars_to_put_by_root var_x_files_l (inc_ml,inc_i,inc_r) =
|l ->
try
let out = List.assoc "." (List.rev_map (fun (p,l,_) -> (p,l)) l) in
- let () = prerr_string "Warning: install rule assumes that -R/-Q . _ is the only -R/-Q option" in
+ let () = prerr_string "Warning: install rule assumes that -R/-Q . _ is the only -R/-Q option\n" in
(None,[".",physical_dir_of_logical_dir out,List.rev_map fst var_x_files_l])
with Not_found ->
(