Merge branch 'fix#5464'
authorJose Pedro Magalhaes <jpm@cs.uu.nl>
Fri, 7 Oct 2011 07:02:26 +0000 (08:02 +0100)
committerJose Pedro Magalhaes <jpm@cs.uu.nl>
Fri, 7 Oct 2011 07:02:26 +0000 (08:02 +0100)

Trivial merge