Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
tools: backport tools/install.py for headers
Backport the tools/install.py changes from 628a3ab that were missed when 6fb0b92 backported the corresponding changes to the Makefile to build the headers only archive.
- Loading branch information