Gary Verhaegen 80652bd51f report-std-change: handle GitHub errors (#4814) ... There have been a few GitHub glitches last week that resulted in a few commits on master not being associated with a PR (though they really were created from merging a PR, and the correct PR number is in their title). This makes the report script crash on not finding the PR, so this PR fixes that. And a comment. CHANGELOG_BEGIN CHANGELOG_END		2020-03-05 10:06:58 +01:00
..
src	Disable pdf docs builds on macos (#4724)	2020-02-26 14:52:08 +00:00
BUILD.bazel	docs cron: follow github pagination links (#4115)	2020-01-20 18:47:47 +01:00
monthly.yaml	report-std-change: handle GitHub errors (#4814)	2020-03-05 10:06:58 +01:00
run.sh	update copyright notices to 2020 (#3939)	2020-01-02 21:21:13 +01:00