diff options
| -rw-r--r-- | debian/changelog | 7 | ||||
| -rwxr-xr-x | debian/rules | 2 |
2 files changed, 8 insertions, 1 deletions
diff --git a/debian/changelog b/debian/changelog index 252138a..addc8c2 100644 --- a/debian/changelog +++ b/debian/changelog @@ -1,3 +1,10 @@ +biniou (1.2.2-2) unstable; urgency=medium + + * Team upload + * Fix build with recent dune + + -- Stéphane Glondu <glondu@debian.org> Sat, 15 Jul 2023 07:17:09 +0200 + biniou (1.2.2-1) unstable; urgency=medium [ Stéphane Glondu ] diff --git a/debian/rules b/debian/rules index 1ad44b0..25fe200 100755 --- a/debian/rules +++ b/debian/rules @@ -16,5 +16,5 @@ override_dh_auto_build: dune build -p biniou override_dh_auto_install: - dune install --destdir=$(DESTDIR) --prefix=/usr --libdir=..$(OCAML_STDLIB_DIR) + dune install --destdir=$(DESTDIR) --prefix=/usr --libdir=$(OCAML_STDLIB_DIR) rm -f $(DESTDIR)/usr/doc/biniou/LICENSE |