diff options
Diffstat (limited to 'scripts/dev/check_doc_changes.py')
| -rwxr-xr-x | scripts/dev/check_doc_changes.py | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/scripts/dev/check_doc_changes.py b/scripts/dev/check_doc_changes.py index f673ad4ea..c1194236a 100755 --- a/scripts/dev/check_doc_changes.py +++ b/scripts/dev/check_doc_changes.py @@ -40,9 +40,9 @@ if code != 0: print() print('(Or you have uncommitted changes, in which case you can ignore ' 'this.)') - if 'TRAVIS' in os.environ: + if 'CI' in os.environ: print() - print("travis_fold:start:gitdiff") + # print("travis_fold:start:gitdiff") subprocess.run(['git', '--no-pager', 'diff'], check=True) - print("travis_fold:end:gitdiff") + # print("travis_fold:end:gitdiff") sys.exit(code) |