Merge remote-tracking branch 'origin/master'
[nmbug-tags.git] / tags / 20111106221554.GA23240@clipper.ens.fr / fixed