-
Paolo Borelli authored
As discussed on IRC with Benjamin, this should not make much difference in practice, but it is more correct
609ddec1
As discussed on IRC with Benjamin, this should not make much difference in practice, but it is more correct