Merge commit 'origin/0.7' into 0.7 0.7 0.7@12288 0.7@12817 trunk@12817
authorroot <root@blitz.inria.fr>
Fri, 2 Jul 2010 15:42:17 +0000 (17:42 +0200)
committerroot <root@blitz.inria.fr>
Fri, 2 Jul 2010 15:42:17 +0000 (17:42 +0200)

Trivial merge