diff options
author | Pierre Courtieu <Pierre.Courtieu@cnam.fr> | 2015-10-19 11:28:30 +0200 |
---|---|---|
committer | Pierre Courtieu <Pierre.Courtieu@cnam.fr> | 2015-10-19 11:28:30 +0200 |
commit | de32427bd2785c365374c554b4b74e97749cb995 (patch) | |
tree | 3894272e3f33c3bd79332f9c0ce3af93eb459790 /lib/pp.ml | |
parent | 289dde7331ee19229b9ba4b9778a76007d93b275 (diff) |
Fixed #4274, bad formatting of messages in emacs mode.
Diffstat (limited to 'lib/pp.ml')
-rw-r--r-- | lib/pp.ml | 4 |
1 files changed, 2 insertions, 2 deletions
@@ -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 |