diff options
| author | Hugo Herbelin | 2020-10-06 00:18:05 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-10-10 22:00:24 +0200 |
| commit | d98cca66ea0e64193e7f79ffcf99b632d0ad6f14 (patch) | |
| tree | 37d88269b02de930a3eb2dc62f6f1cbbcdb94942 /printing/printer.ml | |
| parent | 03d55f990bb7a2c4f5c1fefa408b94a8a93e8d05 (diff) | |
Closes #13142 (more standardized pretty-printing of records).
Diffstat (limited to 'printing/printer.ml')
0 files changed, 0 insertions, 0 deletions