aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
authorMaxime Dénès2017-11-30 15:54:12 +0100
committerMaxime Dénès2017-11-30 15:54:12 +0100
commit0bb126dae41b410fdf4f6531024c64cac20dac06 (patch)
treecc3a9c0d8133eae3902b3a441246d50c48f02436 /dev
parentee45637ac2431fe2df1994f2337d8801e2aeff9a (diff)
parent08da05299d32886bb516124fa497347b40249006 (diff)
Merge PR #6274: Attempt to fix inversion disregarding singleton types (fixes #3125)
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions