diff options
| author | Jim Fehrle | 2018-07-24 15:19:43 -0700 |
|---|---|---|
| committer | Jim Fehrle | 2018-07-29 08:27:44 -0700 |
| commit | d7c52a963588fda638b9f79882a55f56fef6297a (patch) | |
| tree | 35433b197d508e802ea58cf4b0e43954e4344fe2 /plugins/syntax/string_syntax.ml | |
| parent | 535f8ce6edea2e2692f5c9c094d3c6fd07411897 (diff) | |
Fix issue 8132. Print the content of body as in Printer.pr_compacted_decl,
not the type of body. Also update CHANGES to reflect that the argument for Set Diffs
is a string.
Diffstat (limited to 'plugins/syntax/string_syntax.ml')
0 files changed, 0 insertions, 0 deletions