aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/pp.ml
diff options
context:
space:
mode:
authorGravatar Pierre Courtieu <Pierre.Courtieu@cnam.fr>2015-10-19 11:28:30 +0200
committerGravatar Pierre Courtieu <Pierre.Courtieu@cnam.fr>2015-10-19 11:28:30 +0200
commitde32427bd2785c365374c554b4b74e97749cb995 (patch)
tree3894272e3f33c3bd79332f9c0ce3af93eb459790 /lib/pp.ml
parent289dde7331ee19229b9ba4b9778a76007d93b275 (diff)
Fixed #4274, bad formatting of messages in emacs mode.
Diffstat (limited to 'lib/pp.ml')
-rw-r--r--lib/pp.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/lib/pp.ml b/lib/pp.ml
index 1711008ea..4ed4b1779 100644
--- a/lib/pp.ml
+++ b/lib/pp.ml
@@ -362,11 +362,11 @@ let emacs_quote_info_start = "<infomsg>"
let emacs_quote_info_end = "</infomsg>"
let emacs_quote g =
- if !print_emacs then str emacs_quote_start ++ hov 0 g ++ str emacs_quote_end
+ if !print_emacs then hov 0 (str emacs_quote_start ++ g ++ str emacs_quote_end)
else hov 0 g
let emacs_quote_info g =
- if !print_emacs then str emacs_quote_info_start++fnl() ++ hov 0 g ++ str emacs_quote_info_end
+ if !print_emacs then hov 0 (str emacs_quote_info_start++ brk(0,0) ++ g ++ brk(0,0) ++ str emacs_quote_info_end)
else hov 0 g