diff options
Diffstat (limited to 'ide/minilib.mli')
| -rw-r--r-- | ide/minilib.mli | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/ide/minilib.mli b/ide/minilib.mli index b7672c900..4517a2374 100644 --- a/ide/minilib.mli +++ b/ide/minilib.mli @@ -22,7 +22,8 @@ type level = [ (** debug printing *) val debug : bool ref -val log : ?level:level -> string -> unit +val log_pp : ?level:level -> Pp.std_ppcmds -> unit +val log : ?level:level -> string -> unit val coqide_config_home : unit -> string val coqide_config_dirs : unit -> string list |