diff options
Diffstat (limited to 'ide/ideutils.mli')
| -rw-r--r-- | ide/ideutils.mli | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/ide/ideutils.mli b/ide/ideutils.mli index babbfe2f2..0031c59c1 100644 --- a/ide/ideutils.mli +++ b/ide/ideutils.mli @@ -98,3 +98,7 @@ val io_read_all : Glib.Io.channel -> string val run_command : (string -> unit) -> (Unix.process_status -> unit) -> string -> unit + +(* Checks if an error message is printable, it not replaces it with + * a printable error *) +val validate : Pp.t -> Pp.t |