Because the diff was empty but the log was not because of some prior
integration mess.

Before merging something new into next please do
git fetch
git checkout next
git reset --hard origin/next

Martin
_______________________________________________
fenics mailing list
[email protected]
http://fenicsproject.org/mailman/listinfo/fenics

Reply via email to