aboutsummaryrefslogtreecommitdiffhomepage
path: root/stm/spawned.ml
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2017-06-06 00:24:57 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2017-06-06 00:24:57 +0200
commitcc0f9d254c394db742473299336fb20b82ae4aa1 (patch)
treecbc89906c862624d4285f367d1fa9f0f61f16f05 /stm/spawned.ml
parentb377bd30f23f430882902f534eaf31b1314ecd07 (diff)
parent88fdd28815747520bdc555a2d1b8600e114ab341 (diff)
Merge PR#716: Don't double up on periods in anomalies
Diffstat (limited to 'stm/spawned.ml')
-rw-r--r--stm/spawned.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/stm/spawned.ml b/stm/spawned.ml
index c5bd5f6f9..de19dd535 100644
--- a/stm/spawned.ml
+++ b/stm/spawned.ml
@@ -46,7 +46,7 @@ let control_channel = ref None
let channels = ref None
let init_channels () =
- if !channels <> None then CErrors.anomaly(Pp.str "init_channels called twice");
+ if !channels <> None then CErrors.anomaly(Pp.str "init_channels called twice.");
let () = match !main_channel with
| None -> ()
| Some (Socket(mh,mpr,mpw)) ->
@@ -65,7 +65,7 @@ let init_channels () =
| Some (Socket (ch, cpr, cpw)) ->
controller ch cpr cpw
| Some AnonPipe ->
- CErrors.anomaly (Pp.str "control channel cannot be a pipe")
+ CErrors.anomaly (Pp.str "control channel cannot be a pipe.")
let get_channels () =
match !channels with