diff options
Diffstat (limited to 'html/features.html')
| -rw-r--r-- | html/features.html | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/html/features.html b/html/features.html index ad86b3ac..cd8a999c 100644 --- a/html/features.html +++ b/html/features.html @@ -177,6 +177,6 @@ proof assistant to add PBP support.") ?> </dl> <p> For (even) more details of the above features, see the -<?php link_root("doc","documentation page.") ?> +<a href="doc">documentation page</a>. </p> |