diff options
author | Emilio Jesus Gallego Arias <e+git@x80.org> | 2016-12-07 12:12:54 +0100 |
---|---|---|
committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-03-21 15:51:42 +0100 |
commit | 3b3d5937939ac8dc4f152d61391630e62bb0b2e5 (patch) | |
tree | 562c3470d8d2f02226ccf27d032a64a5e9a5dc17 /ide/ideutils.ml | |
parent | 3fc02bb2034a648c9c27b76a9e7b4e02a78e55b9 (diff) |
[pp] [ide] Minor cleanups in pp code.
- We avoid unnecessary use of Pp -> string conversion functions.
and the creation of intermediate buffers on logging.
- We rename local functions that share the name with the Coq stdlib,
this is usually dangerous as if the normal function is removed, code
may pick up the one in the stdlib, with different semantics.
Diffstat (limited to 'ide/ideutils.ml')
-rw-r--r-- | ide/ideutils.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/ide/ideutils.ml b/ide/ideutils.ml index 101f1a5ee..da867e689 100644 --- a/ide/ideutils.ml +++ b/ide/ideutils.ml @@ -337,7 +337,7 @@ let default_logger level message = | Feedback.Warning -> `WARNING | Feedback.Error -> `ERROR in - Minilib.log ~level (Pp.string_of_ppcmds message) + Minilib.log_pp ~level message (** {6 File operations} *) |