tree 561833b6b30ebf54781f69ca8ec2a1681ace19d1
parent 6cd6551b264f720e2b44f0d14e1f78becb002b5e
author Gael Guennebaud <g.gael@free.fr> 1531386429 +0200
committer Gael Guennebaud <g.gael@free.fr> 1531386429 +0200

bug #1570: fix warning