From a5ce47ac0cd3ca10fbd119ff45b226541dc67952 Mon Sep 17 00:00:00 2001
From: David Allsopp <david.allsopp@metastack.com>
Date: Wed, 26 Jun 2019 11:56:47 +0100
Subject: [PATCH] Support Dune 1.7.0 and later

Dune 1.7.0 displays a deprecation warning for jbuild files which needs
to be suppressed when generating the man pages.
---
 doc/Makefile | 3 ++-
 doc/man.sed  | 7 +++++++
 2 files changed, 9 insertions(+), 1 deletion(-)
 create mode 100644 doc/man.sed

diff --git a/doc/Makefile b/doc/Makefile
index 9f00bfd597c..7f627ad8822 100644
--- a/doc/Makefile
+++ b/doc/Makefile
@@ -43,7 +43,8 @@ man:
 	done
 	$(OPAM_INSTALLER) $(HELPFMT) > man/opam-installer.1 2>> man/err
 # Dune doesn't (yet) support --no-print-directory
-	@if grep -v "^Entering directory '" man/err > man/err2 ; then cat man/err2 ; false ; fi
+	@sed -f man.sed man/err > man/err2
+	@if test -s man/err2 ; then cat man/err2 ; false ; fi
 
 man-html: man
 	rm -rf man-html
diff --git a/doc/man.sed b/doc/man.sed
new file mode 100644
index 00000000000..9770bff6df8
--- /dev/null
+++ b/doc/man.sed
@@ -0,0 +1,7 @@
+/^Entering directory '/d
+/^File .*jbuild", line 1, characters 0-0:/{
+  :a
+  N
+  /Note: You can use.*to dune/!ba
+}
+/Warning: jbuild files are deprecated/d