diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-10-19 18:18:34 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-10-19 18:18:34 +0200 |
| commit | c7dcb76ffff6b12b031e906b002b4d76c1aaea50 (patch) | |
| tree | 8d5115258c3b7042767e45d742e2800dab209822 /lib/pp.ml | |
| parent | 666568377cbe1c18ce479d32f6359aa61af6d553 (diff) | |
| parent | 50a574f8b3e7f29550d7abf600d92eb43e7f8ef6 (diff) | |
Merge branch 'v8.5'
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 |