aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/cWarnings.ml
diff options
context:
space:
mode:
Diffstat (limited to 'lib/cWarnings.ml')
-rw-r--r--lib/cWarnings.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/lib/cWarnings.ml b/lib/cWarnings.ml
index 7b8dc2b9b..78fa84f33 100644
--- a/lib/cWarnings.ml
+++ b/lib/cWarnings.ml
@@ -48,7 +48,7 @@ let create ~name ~category ?(default=Enabled) pp =
CErrors.user_err_loc (loc,"_",pp x)
| Enabled ->
let msg =
- pp x ++ str " [" ++ str name ++ str "," ++
+ pp x ++ spc () ++ str "[" ++ str name ++ str "," ++
str category ++ str "]"
in
let loc = Option.default !current_loc loc in