>>>>> On Sat, 6 Apr 2019 23:58:10 +0200, Laura Arjona Reina <larjona@debian.org> 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