diff --git a/ci/check-documentation-diff.py b/ci/check-documentation-diff.py index 088b0bcc4..a306a743d 100755 --- a/ci/check-documentation-diff.py +++ b/ci/check-documentation-diff.py @@ -13,7 +13,7 @@ if __name__ == "__main__": with open(diffname, 'w') as diff: subprocess.check_call(['git', 'diff'], stdout=diff) print('\033[91mYou have a diff in the documentation cache. Please update with:\033[0m') - print(' $ curl %s/%s | git apply -' % (os.environ['CI_ARTIFACTS_URL'], diffname.replace('../', ''))) + print(' $ curl -L %s/%s | git apply -' % (os.environ['CI_ARTIFACTS_URL'], diffname.replace('../', ''))) if res != 0: print('(note that it might take a few minutes for artefacts to be available on the server)\n')