>>>>> On Sat, 6 Apr 2019 23:58:10 +0200, Laura Arjona Reina >>>>> <[email protected]> said:
> I still have no opinion about this bug, I'll try to put time on getting
> #922222 fixed first
Hi Laura,
in #922222 you propose excatly what I like to do with the problematic
manuals on /doc/ddp:
"remove them from the "7doc_manuals" build script" and
"change the link to point to the corresponding attic repo".
--
regards Thomas
