HomeSoftware Heritage

Makefile: prefer "make docs" over "make doc", as it is the convention

Description

Makefile: prefer "make docs" over "make doc", as it is the convention

Details

Provenance
zackAuthored on Sep 5 2017, 11:31 AM
zackPushed on Sep 5 2017, 11:33 AM
Parents
rDENVf09abfb71a29: Makefile: add proxy "doc" target to build HTML Sphynx doc
Branches
Unknown
Tags
Unknown