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