Fix some small things broken with the last merge.
authorJose Pedro Magalhaes <jpm@cs.uu.nl>
Thu, 12 May 2011 13:48:45 +0000 (15:48 +0200)
committerJose Pedro Magalhaes <jpm@cs.uu.nl>
Thu, 12 May 2011 13:48:45 +0000 (15:48 +0200)

No differences found