Ignore error if nothing to commit

[jdahm]

Purpose

Fix push_docs by ignoring error if there is nothing to commit.

I checked and git push returns 0 if there is nothing to push, so this should be all that is needed to avoid the test "failure".

[FlorianDeconinck]

launch jenkins