aboutsummaryrefslogtreecommitdiff
path: root/html/features.html
diff options
context:
space:
mode:
authorDavid Aspinall2000-09-29 17:47:34 +0000
committerDavid Aspinall2000-09-29 17:47:34 +0000
commit0343b2b7187a599d2373e92e00d5e8ad7da91c3f (patch)
treef2a8ed42df461e6cd9171a5bce55792172cea98f /html/features.html
parent4e2c1e49359fdc4f1dbb0fe31b182c6d8e09eaae (diff)
Remove messy link_root links.
Diffstat (limited to 'html/features.html')
-rw-r--r--html/features.html2
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>