diff --git a/doc/docutil.php b/doc/docutil.php
index f601776515..6d5d7f9904 100644
--- a/doc/docutil.php
+++ b/doc/docutil.php
@@ -29,24 +29,22 @@ function page_head($title) {
}
function copyright() {
+ $y = date("Y ");
echo "
- Copyright © $y University of California
- ";
- return;
- echo "
-
-
-
+
+ Copyright © $y University of California.
+ Permission is granted to copy, distribute and/or modify this document
+ under the terms of the GNU Free Documentation License,
+ Version 1.2 or any later version published by the Free Software Foundation.
";
}
function page_tail() {
- $y = date("Y ");
echo "