diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-07-20 14:44:21 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-07-20 14:44:21 +0200 |
| commit | b02179e15d35352b48440657ad47f6bf7ee9495c (patch) | |
| tree | 7e3875d28a0b80d7be489460ede13457c475fa9c /lib/pp.ml | |
| parent | f25613e8a2a6c9264650cb0be891bb073979c67d (diff) | |
| parent | a2bfcf3ca588d1622655cc13713bc6f5d339b86d (diff) | |
Merge PR #898: [pp] Fix bugs 5651 [incorrect thunk in pretty printer]
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 |