[issue13810] refer people to Doc/Makefile when not using 'make' to build main documentation

[Sandro Tosi]

Sandro Tosi <sandro.tosi at gmail.com> added the comment:

The outdated command is addressed in issue#12415, and I think it's better to provide a precise command in devguide, so that if you don't use make you don't even need to understand where to grab the information to checkout third-party tools.

Additionally, the whole way we're fetching those tools will be revisited soon.

----------
nosy: +sandro.tosi
resolution:  -> duplicate
stage:  -> committed/rejected
status: open -> closed
superseder:  -> Missing: How to checkout the Doc sources

_______________________________________
Python tracker <report at bugs.python.org>
<http://bugs.python.org/issue13810>
_______________________________________