aboutsummaryrefslogtreecommitdiffstats
path: root/driver
diff options
context:
space:
mode:
authorxleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2009-08-18 06:31:17 +0000
committerxleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2009-08-18 06:31:17 +0000
commit22d65c5931d702f6e2abde9b3b7d822b8d3c5560 (patch)
treeb0501324887c4fb3b9493a5e9aaffa4f7de39fe8 /driver
parent24a8dbb62e8171f3f3ad87e8d3f697e726df0e6a (diff)
downloadcompcert-22d65c5931d702f6e2abde9b3b7d822b8d3c5560.tar.gz
compcert-22d65c5931d702f6e2abde9b3b7d822b8d3c5560.zip
No '\n' in Coq strings...
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1129 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'driver')
-rw-r--r--driver/Driver.ml4
1 files changed, 3 insertions, 1 deletions
diff --git a/driver/Driver.ml b/driver/Driver.ml
index 8361829f..30d4a6cc 100644
--- a/driver/Driver.ml
+++ b/driver/Driver.ml
@@ -39,7 +39,9 @@ let print_error oc msg =
let print_one_error = function
| Errors.MSG s -> output_string oc (Camlcoq.camlstring_of_coqstring s)
| Errors.CTX i -> output_string oc (Camlcoq.extern_atom i)
- in List.iter print_one_error msg
+ in
+ List.iter print_one_error msg;
+ output_char oc '\n'
(* For the CIL -> Csyntax translator: