Merge "TitleOptionWidget: Documentation type fix"
authorjenkins-bot <jenkins-bot@gerrit.wikimedia.org>
Tue, 20 Aug 2019 15:20:13 +0000 (15:20 +0000)
committerGerrit Code Review <gerrit@wikimedia.org>
Tue, 20 Aug 2019 15:20:13 +0000 (15:20 +0000)
commit34db5e10c0c1695d0a35190e101fa2434f9bbbb8
tree24b8bbd4a46c477cc1c34f56c2a784a38150eb3a
parentdcb26aa2dbf360fec1382a95161eaf0420bc60ad
parent6a12506c68138898264388b0d8f85f293fc9de4e
Merge "TitleOptionWidget: Documentation type fix"