diff options
Diffstat (limited to 'contrib/correctness/pmisc.ml')
| -rw-r--r-- | contrib/correctness/pmisc.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/correctness/pmisc.ml b/contrib/correctness/pmisc.ml index 6d04befe2..36e4f0dc9 100644 --- a/contrib/correctness/pmisc.ml +++ b/contrib/correctness/pmisc.ml @@ -22,7 +22,7 @@ let debug = ref false let deb_mess s = if !debug then begin - mSGNL s; pp_flush() + msgnl s; pp_flush() end let list_of_some = function |