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)
* master:
  Makefile, bin/chroot-maint: Keep `/usr/local/include' mostly empty.


Trivial merge