diff --git a/docs/devinfo.html b/docs/devinfo.html index 5c03344b49b..7176824efd1 100644 --- a/docs/devinfo.html +++ b/docs/devinfo.html @@ -197,6 +197,8 @@ branch is relevant.