From 34f43b4dd4111c9e5220b1408270e4d4d5f4ce2d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr> Date: Tue, 2 Apr 2019 14:30:25 +0200 Subject: [PATCH] [Eva] Fixes a comment. --- src/plugins/value/value_parameters.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/plugins/value/value_parameters.ml b/src/plugins/value/value_parameters.ml index ee36c857ced..82314cb1807 100644 --- a/src/plugins/value/value_parameters.ml +++ b/src/plugins/value/value_parameters.ml @@ -1336,8 +1336,8 @@ module Precision = let () = Precision.set_range (-1) 11 let () = add_precision_dep Precision.parameter -(* Sets a parameter [P] to [t], unless it has already been set by another mean - that this function. *) +(* Sets a parameter [P] to [t], unless it has already been set by any other + means. *) let set (type t) (module P: Parameter_sig.S with type t = t) = let previous = ref (P.get ()) in fun t -> -- GitLab