Merge commit 'origin/master'
authorroot <root@blitz.inria.fr>
Wed, 17 Nov 2010 21:25:53 +0000 (22:25 +0100)
committerroot <root@blitz.inria.fr>
Wed, 17 Nov 2010 21:25:53 +0000 (22:25 +0100)
commita0b98745bd9a073d3ff9a91e33cbab0904dbfdf2
tree99d5f005475ad84cf0438909fa3be06870f6594a
parent32e6b3ac389e522e05b89833e9bd13ad853b6885
parentcb7f7cf50f9a7354c7984ee5502e7e3807b639b3
Merge commit 'origin/master'