Merge branch 'master' of git@git.tuebingen.mpg.de:libdai
authorJoris Mooij <joris.mooij@tuebingen.mpg.de>
Tue, 3 Mar 2009 08:42:22 +0000 (09:42 +0100)
committerJoris Mooij <joris.mooij@tuebingen.mpg.de>
Tue, 3 Mar 2009 08:42:22 +0000 (09:42 +0100)

Trivial merge