aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile.ci
diff options
context:
space:
mode:
authorGravatar Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>2018-03-09 13:20:54 +0100
committerGravatar Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>2018-03-09 16:30:12 +0100
commit65cba7c6cb1016df13e948452f1e3cb58edcb996 (patch)
treee70a8f42e040b0382db09e71c8a93c3682a683aa /Makefile.ci
parentaf5eded304b74fa0fccb35a7dc284c46a96ba5cc (diff)
Adjust EConstr.cmp_constructors for relaxed constructor cumulativity
Diffstat (limited to 'Makefile.ci')
0 files changed, 0 insertions, 0 deletions