diff --git a/docs/ReleaseNotes.html b/docs/ReleaseNotes.html index 7402d90b997..2055e5feaf0 100644 --- a/docs/ReleaseNotes.html +++ b/docs/ReleaseNotes.html @@ -89,6 +89,7 @@ the C front-end.