http://gcc.gnu.org/bugzilla/show_bug.cgi?id=47145
--- Comment #26 from Benjamin Kosnik <bkoz at gcc dot gnu.org> 2011-03-22 08:59:02 UTC --- Matthias, this should allow you to remove the current debian docs patch. Does it?
http://gcc.gnu.org/bugzilla/show_bug.cgi?id=47145
--- Comment #26 from Benjamin Kosnik <bkoz at gcc dot gnu.org> 2011-03-22 08:59:02 UTC --- Matthias, this should allow you to remove the current debian docs patch. Does it?