diff --git a/.travis/pushdoc b/.travis/pushdoc
index d794006807a4a3b3643641334e001c635238c015..6f69d7c41ac6c092e7075bd251e88b8ca9d9c561 100755
--- a/.travis/pushdoc
+++ b/.travis/pushdoc
@@ -6,6 +6,11 @@ set -x
 GIT_OWNER=$(  echo $TRAVIS_REPO_SLUG | sed "s/\/.*$//" )
 GIT_REPO=$(   echo $TRAVIS_REPO_SLUG | sed "s/^.*\///" )
 
+if [ "$TRAVIS_PULL_REQUEST" != false ] ; then
+  echo "Building from a pull request, nothing to push"
+  exit 0
+fi
+
 if [ "$GIT_OWNER" = plumed ] ; then
   if [[ "$TRAVIS_BRANCH" =~ ^v2\.[0-9]+$ ]] ; then
     if test -f CHANGES/"$TRAVIS_BRANCH".md && grep -q plumednotmaintained CHANGES/"$TRAVIS_BRANCH".md ; then