chiark / gitweb /
Merge branch 'master' into deploy.spirit
authorMark Wooding <mdw@distorted.org.uk>
Sat, 9 May 2020 16:01:26 +0000 (17:01 +0100)
committerMark Wooding <mdw@distorted.org.uk>
Sat, 9 May 2020 16:01:26 +0000 (17:01 +0100)
commitc9cd31f4ef641e602f34548a51b6b0ab4e72961a
tree43aea27b4d2ae446c71ed332f7f97239e5eab720
parent76b8f63e9069432b591f70598792e6a00ec795ea
parent942fed180961536fa966bfd4db28ee0537755932
Merge branch 'master' into deploy.spirit

* master:
  Makefile, bin/chroot-maint: Keep `/usr/local/include' mostly empty.