> A removed check in ba3deeefb
Indeed. It seems that it was really removed by 1bc90f7a, that I should have checked...
-- Fabien.