[gcc/devel/sphinx] (2 commits) Merge branch 'master' into devel/sphinx

[Martin Liska]

The branch 'devel/sphinx' was updated to point to:

 2912c844bc7... Merge branch 'master' into devel/sphinx

It previously pointed to:

 af458885cf3... Merge branch 'master' into devel/sphinx

Diff:

Summary of changes (added commits):
-----------------------------------

  2912c84... Merge branch 'master' into devel/sphinx
  cff8fa9... docs: Use https in manual. (*)

(*) This commit already exists in another branch.
    Because the reference `refs/heads/devel/sphinx' matches
    your hooks.email-new-commits-only configuration,
    no separate email is sent for this commit.