Merge branches 'devel' and 'master' into debian-devel
authorBarak A. Pearlmutter <barak+git@cs.nuim.ie>
Tue, 13 Aug 2013 10:50:33 +0000 (12:50 +0200)
committerBarak A. Pearlmutter <barak+git@cs.nuim.ie>
Tue, 13 Aug 2013 10:50:33 +0000 (12:50 +0200)
commit477ae6291a796b48edfbe7d4fd16744f9d05ff30
tree9277195ee746587a9089c3aa4ecfdc8951677b1d
parentaea847a2c3331614a9875de43e9470cc9d33fde4
parentcfae5e57908615750d45d45233dbe395a81539da
parent4b34cc271020941807398afdf0b04a956f1d1dfe
Merge branches 'devel' and 'master' into debian-devel