On Tue, Jun 26, 2012 at 01:25:24PM +0200, Johan Hake wrote: > On 06/26/2012 12:57 PM, Anders Logg wrote: > >Yes, that would be a very good idea. Feel free to push a fix. :-) > > Already done locally. Waiting for the buildbots now :)
Push fixed so it should be ok to push now. -- Anders _______________________________________________ Mailing list: https://launchpad.net/~dolfin Post to : dolfin@lists.launchpad.net Unsubscribe : https://launchpad.net/~dolfin More help : https://help.launchpad.net/ListHelp
