diff options
| -rw-r--r-- | typing/printtyp.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/typing/printtyp.ml b/typing/printtyp.ml index 462920ff5..d015c99aa 100644 --- a/typing/printtyp.ml +++ b/typing/printtyp.ml @@ -549,7 +549,8 @@ and modtype_declaration id decl = let signature sg = open_vbox 0; signature_body false sg; - close_box() + close_box(); + print_newline() (* Print an unification error *) |