diff options
author | bors[bot] <26634292+bors[bot]@users.noreply.github.com> | 2019-12-03 14:02:23 +0000 |
---|---|---|
committer | GitHub <[email protected]> | 2019-12-03 14:02:23 +0000 |
commit | 15f143f0c33cbd382a2ad7a407d9601cb843d164 (patch) | |
tree | 0a357e2d3333a06e37f5cb8d6613733c1c0c78ac /.gitattributes | |
parent | ba4f7fa02f746e5bb3efdaa06c2b35beaa4e3440 (diff) | |
parent | e4add45951511f9afe348bf6066a724deb0d3ccf (diff) |
Merge #2468
2468: Fix #2467 r=flodiebold a=flodiebold
The stand-alone `unify` requires that the type doesn't contain any type
variables. So we can't share the code here for now (without more refactoring)...
Co-authored-by: Florian Diebold <[email protected]>
Diffstat (limited to '.gitattributes')
0 files changed, 0 insertions, 0 deletions