diff --git a/docs/ReleaseNotes.html b/docs/ReleaseNotes.html index 5730ec1051a..ba950536bac 100644 --- a/docs/ReleaseNotes.html +++ b/docs/ReleaseNotes.html @@ -139,11 +139,14 @@ the C backend.