diff options
author | Johannes Schindelin <johannes.schindelin@gmx.de> | 2020-10-11 21:27:10 +0000 |
---|---|---|
committer | Junio C Hamano <gitster@pobox.com> | 2020-10-12 12:27:10 -0700 |
commit | d0ff1a3cbc579947c5daeeb5ac433885a0bdc88e (patch) | |
tree | 889107108bbe3710d26db27977080904e7f1349d /Documentation/config/color.txt | |
parent | ci: do not skip tagged revisions in GitHub workflows (diff) | |
download | tgif-d0ff1a3cbc579947c5daeeb5ac433885a0bdc88e.tar.xz |
ci: work around old records of GitHub runs
Apparently older GitHub runs at least _sometimes_ lack information about
the `head_commit` (and therefore the `ci-config` check will fail with
"TypeError: Cannot read property 'tree_id' of null") in the check added
in 7d78d5fc1a9 (ci: skip GitHub workflow runs for already-tested
commits/trees, 2020-10-08).
Let's work around this by adding a defensive condition.
Reported-by: Philippe Blain <levraiphilippeblain@gmail.com>
Signed-off-by: Johannes Schindelin <johannes.schindelin@gmx.de>
Signed-off-by: Junio C Hamano <gitster@pobox.com>
Diffstat (limited to 'Documentation/config/color.txt')
0 files changed, 0 insertions, 0 deletions