diff options
| author | Damien George <damien.p.george@gmail.com> | 2020-04-19 21:09:22 +1000 |
|---|---|---|
| committer | Damien George <damien.p.george@gmail.com> | 2020-04-22 14:03:07 +1000 |
| commit | 1cc24cd39a971a03fe397ce575e59aa7d9b48e3b (patch) | |
| tree | ed4bb70588e72652647b11af07f4cef2c7a7faa8 /docs | |
| parent | a4423570e2421c61886e7e28333298042bb349a2 (diff) | |
tools/metrics.py: Don't build mpy-cross if not needed by any ports.
To save build time.
Diffstat (limited to 'docs')
0 files changed, 0 insertions, 0 deletions