From 8f19f4805ac01b529f43483e6aa224267e9f1e33 Mon Sep 17 00:00:00 2001
From: P. J. McDermott <pjm@nac.net>
Date: Wed, 30 May 2012 16:31:17 -0400
Subject: Edit description of documentation repositories.

---
diff --git a/dev.html b/dev.html
index 5300fd1..671ba92 100755
--- a/dev.html
+++ b/dev.html
@@ -5,8 +5,8 @@
 <dl>
 	<dt><a href="http://git.os.pehjota.net/pkg/">Packages in Git</a></dt>
 	<dd>Most source packages are maintained in Git repositories.  To assist in the maintenance of a package, coordinate with its maintainer(s) and the <a href="http://www.pehjota.net/contact.html">system administrator</a>.</dd>
-	<dt><a href="http://git.os.pehjota.net/doc/">Notes, specifications, and policies</a></dt>
-	<dd>Specifications and policies are maintained in Git repositories.</dd>
+	<dt><a href="http://git.os.pehjota.net/doc/">Documentation</a></dt>
+	<dd>Notes, specifications, and policies are maintained in Git repositories.</dd>
 	<dt><a href="http://git.os.pehjota.net/www/">Web site</a></dt>
 	<dd>These Web pages are maintained in a Git repository.</dd>
 </dl>
--
cgit v0.9.1