Avoid full CI if no change in source

[albinahlback]

As described by Dimitri in #2425 (comment)

[fredrik-johansson]

Conversely, it would be nice to test that building the docs works in CI in PRs, at least when the docs have changed. Currently the Deploy / Push documentation job fails because I messed up in #2417.