diff options
| author | Emilio Jesus Gallego Arias | 2018-12-10 14:56:23 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-12-10 14:56:23 +0100 |
| commit | 10b07a187522b74bbcc9355d3ff9c4153f300706 (patch) | |
| tree | 62fce42c8fec43f263de60be71ab0a51fdbf9b6a /lib | |
| parent | 3f014b0c883cd71cf751b0ccc297edb38e46ae47 (diff) | |
| parent | fb81b677b546e2e596f411195684ba47ebe67d91 (diff) | |
Merge PR #9145: Do so that an error message follows the "Error:" header on the same line
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/cErrors.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/lib/cErrors.ml b/lib/cErrors.ml index 811fcf4063..79f0a806a7 100644 --- a/lib/cErrors.ml +++ b/lib/cErrors.ml @@ -112,7 +112,7 @@ let iprint_no_report (e, info) = let _ = register_handler begin function | UserError(s, pps) -> - hov 0 (where s ++ pps) + where s ++ pps | _ -> raise Unhandled end |