Merge branch 'master' of git.tuebingen.mpg.de:libdai
authorJoris Mooij <joris.mooij@tuebingen.mpg.de>
Mon, 6 Jun 2011 18:58:15 +0000 (20:58 +0200)
committerJoris Mooij <joris.mooij@tuebingen.mpg.de>
Mon, 6 Jun 2011 18:58:15 +0000 (20:58 +0200)

Trivial merge