diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-07-19 14:36:37 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-07-19 14:36:37 +0200 |
| commit | a2bfcf3ca588d1622655cc13713bc6f5d339b86d (patch) | |
| tree | 1b5e7dac682693d0c4bf1347f69c7252545004e9 /lib/pp.ml | |
| parent | 28b3bfd84718e5b29f8e3452fcfe22b19e9910dd (diff) | |
[pp] Fix bugs 5651 [incorrect thunk in pretty printer]
Fix bug introduced by a Haskell programmer.
Diffstat (limited to 'lib/pp.ml')
| -rw-r--r-- | lib/pp.ml | 4 |
1 files changed, 2 insertions, 2 deletions
@@ -153,7 +153,7 @@ let rec pr_com ft s = | None -> () (* pretty printing functions *) -let pp_with ft = +let pp_with ft pp = let cpp_open_box = function | Pp_hbox n -> Format.pp_open_hbox ft () | Pp_vbox n -> Format.pp_open_vbox ft n @@ -175,7 +175,7 @@ let pp_with ft = pp_cmd s; pp_close_tag ft () in - try pp_cmd + try pp_cmd pp with reraise -> let reraise = Backtrace.add_backtrace reraise in let () = Format.pp_print_flush ft () in |