Created
March 21, 2022 10:46
-
-
Save Octachron/31f4af1e605747e130f2290ded798c89 to your computer and use it in GitHub Desktop.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| let device_flush ppf = | |
| let fs = Format.pp_get_formatter_out_functions ppf () in | |
| fs.out_flush () | |
| let force_break_hints ppf = | |
| let margin = Format.pp_get_margin ppf () in | |
| Format.pp_print_as ppf (margin+1) "" | |
| let gentler_flush ppf = | |
| force_break_hints ppf; device_flush ppf |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment