tree d245384358a911c9cab259873e035997ca49ce6c
parent d4929ed324d7effa17389cd641bc4c55a08822ed
parent 3bb7a30f76321cea1945088d0b448b02d07c05fe
author bors[bot] <26634292+bors[bot]@users.noreply.github.com> 1592851830 +0000
committer GitHub <noreply@github.com> 1592851830 +0000
gpgsig -----BEGIN PGP SIGNATURE-----
 
 wsBcBAABCAAQBQJe8P12CRBK7hj4Ov3rIwAAdHIIAACz5EIi//M96o6sBdtsxRRJ
 ltlBzf3Zi7c8JBY7cUrYPy4eS93t1WUbJu7NiLPfdIFrnzLaMsVb9QXZCfNq0yIS
 lqyybSS61VVBLpAoGO+pELEylFhEhq54FHJU8jaqQ3pSQiLXA8/sRQVTmXD+zdgg
 e4Qq0i/yXBrJJFTvQFVsaiCDNFjHxnhBMB2kXf9YW7xwFefrditG9NhLg7q/0VUr
 M246hCties2Doh8Ov1i0P510hdItsaeEUo+Aeg4TYIsuPPI1iSxCIl7+XtOTDiF8
 3nhisW+j7l3PdJSad8Zhs/hGXPpdDtwXx9EPXLV9+4J2ihtpHKxSKR7yb4Ljld0=
 =FaxY
 -----END PGP SIGNATURE-----
 

Merge #203

203: Add a CI tool that prints a size diff for incoming PRs. r=jrvanwhy a=jrvanwhy

The diff is computed by building the examples with `make examples` both in the PR's target branch and the merge result, and running `diff` on the result.

This is built using GitHub Actions because upstream Tock is moving to GitHub Actions (see https://github.com/tock/tock/pull/1815, and [this core WG discussion](https://github.com/tock/tock/blob/master/doc/wg/core/notes/core-notes-2020-04-24.md#ci-infrastructure-travis-to-github-actions)).

Co-authored-by: Johnathan Van Why <jrvanwhy@google.com>