chiark / gitweb /
Merge branch 'ci' into 'main'
authorIan Jackson <iwj@debian.org>
Thu, 15 Jun 2023 11:48:31 +0000 (11:48 +0000)
committerIan Jackson <iwj@debian.org>
Thu, 15 Jun 2023 11:48:31 +0000 (11:48 +0000)
CI: check that build-deps in d/control are as autogenerated

See merge request iwj/hippotat!3


Trivial merge