docs/Makefile: Remove no longer needed target

It enables to successfully invoke make in the docs folder.

---

Migrated from D5547 (view on Phabricator)

Build is green

Patch application report for D5547 (id=19796)

Rebasing onto 282e7f19...

Current branch diff-target is up to date.

Changes applied before test

commit 227c78ca28c7ef170d1265f538ce95efd7e7132e
Author: Antoine Lambert <antoine.lambert@inria.fr>
Date:   Fri Apr 16 14:22:39 2021 +0200

    docs/Makefile: Remove no longer needed target
    
    It enables to successfully invoke make in the docs folder.

See https://jenkins.softwareheritage.org/job/DLDBASE/job/tests-on-diff/474/ for more details.

Merge request was accepted

approved this merge request

Merge request was merged

closed