diff options
| author | Maxime Dénès | 2016-06-27 15:05:29 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2016-06-27 15:06:42 +0200 |
| commit | 653e5307c846079a4ba3d2392fc55158ea4ee3c6 (patch) | |
| tree | 8f12fda9671aafa5c05846ab1eed1a4107727785 /plugins | |
| parent | 13af70bece67a6d8f9fcd06cedf24bb2f0dc279a (diff) | |
| parent | c83fa10156545bce96ef4a0f93e8695ec353c834 (diff) | |
Merge branch 'sort-fields' into trunk
Was PR#86 Simplify `interp/constrintern.ml:sort_fields`.
Diffstat (limited to 'plugins')
0 files changed, 0 insertions, 0 deletions