Docs: cancel PR builds if there is no documentation changes

[humitos]

Use the new feature to cancel builds if there are not documentation changes

[benjaoming]

LGTM! We should also be running this ASAP in production to make sure that we gather maximum hands-on experience with the approach :)

[benjaoming]

@humitos we'll have to investigate why the latest build fails with exit code 1: https://readthedocs.org/projects/dev/builds/18636879/

[humitos]

Meh, this doesn't work as we expected. When git diff returns 1 it exists immediately and break the build. We need a way to execute the git diff command and save its exit code into a variable without exiting the whole command.

[benjaoming]

If you want the one-liner, you can use ! git diff --quiet origin/main -- docs/ || exit 183

[humitos]

I don't think that works either. Have you tested it?

[humitos]

Cool! I figured it out. My last command change worked! 💪🏼

[benjaoming]

I don't think that works either. Have you tested it?

Yes, worked fine locally 👍

[benjaoming]

Since this does change docs/, we should remember to check that it actually "skips" builds after it's been merged :)