Actually fix Gitlab doc build
commita41df09d4adc2500a4e65dbf7f05b75b4afde515
authorPaul Bauer <paul.bauer.q@gmail.com>
Fri, 17 Jan 2020 11:54:26 +0000 (17 12:54 +0100)
committerPaul Bauer <paul.bauer.q@gmail.com>
Fri, 17 Jan 2020 14:04:45 +0000 (17 15:04 +0100)
treeca63e6d091c5e09bdb519077182fd17b4e76616d
parent658765317fd94df5d534c039462be03ab3839067
Actually fix Gitlab doc build

Was still failing after 658765317fd94df5d534c039462be03ab3839067 got
merged.

Actually fixes #3278

Change-Id: I747fe5c677864d1f50ab97d0eda38c68a6085b45
docs/dev-manual/jenkins.rst
docs/dev-manual/releng/index.rst