aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2021-01-07 00:18:16 +0100
committerPierre-Marie Pédrot2021-01-12 13:20:29 +0100
commitb721752d10969dc70eb21ddad9d794042ea34c59 (patch)
tree4cb82b137264022463461e01407b31ddf28551a2 /dev
parent71b5649acf83acb3fe6f1c5ddc468d5c504b7983 (diff)
Slight tweak of the matching algorithm for PIf vs. Case.
It is equivalent but makes the code more similar to the PCase vs. Case case (aha).
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions