Fix compilation with recent dune
authorJulien Puydt <jpuydt@debian.org>
Thu, 6 Jul 2023 07:36:23 +0000 (09:36 +0200)
committerJulien Puydt <jpuydt@debian.org>
Thu, 6 Jul 2023 07:36:23 +0000 (09:36 +0200)
commit60f37e2e3977cf4854224a822627c7cd7d56cc88
tree6bbf5fedc0401ca8a6a28ca5be9d5c4f85b5d230
parent12840bacb96ec4238d355bf25fd3611ddb0d3c92
Fix compilation with recent dune
debian/changelog
debian/rules