aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/remoteCounter.ml
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2017-05-31 12:30:50 -0400
committerGravatar Jason Gross <jgross@mit.edu>2017-06-02 20:06:05 -0400
commit6a67a0e30bdd96df994dd7d309d1f0d8cc22751f (patch)
tree7f0f8129d69a3dd4fdeacf30dd773bc42e9a95f6 /lib/remoteCounter.ml
parent42d510ceea82d617ac4e630049d690acbe900688 (diff)
Drop '.' from CErrors.anomaly, insert it in args
As per https://github.com/coq/coq/pull/716#issuecomment-305140839 Partially using ```bash git grep --name-only 'anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp.\)\?(\(\(Pp.\)\?str\)\?\s*".*[^\.!]")' | xargs sed s'/\(anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp.\)\?(\(\(Pp.\)\?str\)\?\s*".*\s*[^\.! ]\)\s*")/\1.")/g' -i ``` and ```bash git grep --name-only ' !"' | xargs sed s'/ !"/!"/g' -i ``` The rest were manually edited by looking at the results of ```bash git grep anomaly | grep '\.ml' | grep -v 'anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp\.\)\?(\(\(Pp.\)\?str\)\?\s*".*\(\.\|!\)")' | grep 'anomaly\($\|[^_]\)' | less ```
Diffstat (limited to 'lib/remoteCounter.ml')
-rw-r--r--lib/remoteCounter.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/lib/remoteCounter.ml b/lib/remoteCounter.ml
index e7646fb79..11f151a60 100644
--- a/lib/remoteCounter.ml
+++ b/lib/remoteCounter.ml
@@ -25,7 +25,7 @@ let new_counter ~name a ~incr ~build =
(* - in the main process there is a race condition between slave
managers (that are threads) and the main thread, hence the mutex *)
if Flags.async_proofs_is_worker () then
- CErrors.anomaly(Pp.str"Slave processes must install remote counters");
+ CErrors.anomaly(Pp.str"Slave processes must install remote counters.");
Mutex.lock m; let x = f () in Mutex.unlock m;
build x in
let mk_thsafe_remote_getter f () =
@@ -33,7 +33,7 @@ let new_counter ~name a ~incr ~build =
let getter = ref(mk_thsafe_local_getter (fun () -> !data := incr !!data; !!data)) in
let installer f =
if not (Flags.async_proofs_is_worker ()) then
- CErrors.anomaly(Pp.str"Only slave processes can install a remote counter");
+ CErrors.anomaly(Pp.str"Only slave processes can install a remote counter.");
getter := mk_thsafe_remote_getter f in
(fun () -> !getter ()), installer