diff options
| -rw-r--r-- | docs/ReleaseNotes.html | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/docs/ReleaseNotes.html b/docs/ReleaseNotes.html index 9552fe701a..9174e9142e 100644 --- a/docs/ReleaseNotes.html +++ b/docs/ReleaseNotes.html @@ -209,7 +209,7 @@ Release Notes</a>.</h1> <!--=========================================================================--> <h3> -<a name="Polly">Polly</a> +<a name="Polly">Polly: Polyhedral Optimizer</a> </h3> <div> |