diff --git a/docs/ProgrammersManual.html b/docs/ProgrammersManual.html
index bde2ae03d33..9661b769357 100644
--- a/docs/ProgrammersManual.html
+++ b/docs/ProgrammersManual.html
@@ -803,7 +803,7 @@ vector is also useful when interfacing with code that expects vectors :).
 <div class="doc_code">
 <pre>
 for ( ... ) {
-   std::vector<foo> V;
+   std::vector&lt;foo&gt; V;
    use V;
 }
 </pre>
@@ -813,7 +813,7 @@ for ( ... ) {
 
 <div class="doc_code">
 <pre>
-std::vector<foo> V;
+std::vector&lt;foo&gt; V;
 for ( ... ) {
    use V;
    V.clear();