really refresh patches against tip

diff --git a/debian/patches/debian-specific/build_doc_adjustments.diff b/debian/patches/debian-specific/build_doc_adjustments.diff
index de01fc7e67689c25894c02f87b2cb7cd550fb67d..0618fa4fc44f98f0376a75a3760b91b09d12c448 100644 (file)
--- a/debian/patches/debian-specific/build_doc_adjustments.diff
+++ b/debian/patches/debian-specific/build_doc_adjustments.diff
@@ -1,12 +1,14 @@
 --- a/doc/Makefile.am
 +++ b/doc/Makefile.am
-@@ -81,13 +81,14 @@ uninstall-local:
+@@ -81,15 +81,16 @@ uninstall-local:
  
  check:
  manual.txt: manual.html
--      -lynx -dump -nolist -with_backspaces $^ > $@ || w3m -dump $^ > $@
+-      -lynx -dump -nolist -with_backspaces $^ > $@ || \
 +      links.main -dump $^ > $@ || links -dump $^ > $@ || \
-+      lynx -dump -nolist -with_backspaces $^ > $@ || w3m -dump $^ > $@
++      lynx -dump -nolist -with_backspaces $^ > $@ || \
+       w3m -dump $^ > $@ || \
+       elinks -dump -no-numbering -no-references $^ > $@
  
  manual.html: $(srcdir)/html.xsl stamp-doc-xml
 -      -xsltproc --nonet -o $@ $(srcdir)/html.xsl manual.xml