[PATCH 03/26] docs/devel: fix duplicate line