aboutsummaryrefslogtreecommitdiffstats
path: root/backend/AisAnnot.ml
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2018-03-09 15:33:30 +0100
committerBernhard Schommer <bernhardschommer@gmail.com>2018-03-09 15:33:30 +0100
commit96913f741fa9bb31502e32178d67f9efb81033c3 (patch)
tree30880121d48f8f2d90a67893ad8be0279cc41280 /backend/AisAnnot.ml
parenta45ddea290008a8a340f3a2b076268e04f80bab4 (diff)
downloadcompcert-kvx-96913f741fa9bb31502e32178d67f9efb81033c3.tar.gz
compcert-kvx-96913f741fa9bb31502e32178d67f9efb81033c3.zip
Added seperator in warning msg. Bug 23179
Diffstat (limited to 'backend/AisAnnot.ml')
-rw-r--r--backend/AisAnnot.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/backend/AisAnnot.ml b/backend/AisAnnot.ml
index c5fade24..4c637922 100644
--- a/backend/AisAnnot.ml
+++ b/backend/AisAnnot.ml
@@ -140,7 +140,7 @@ let ais_annot_txt warn lbl preg_string sp_reg_name txt args =
| Bad_parameter s ->
if warn then begin
let loc = loc_of_txt txt in
- warning loc Wrong_ais_parameter "wrong ais parameter %s" s
+ warning loc Wrong_ais_parameter "wrong ais parameter: %s" s
end;
[]
in