On Thu, 2008-06-26 at 18:01 +0000, Russ Allbery wrote: > The following commit has been merged in the master branch: > commit d2bda16c93c7b619ee593ae3908ca579b8600c50 > Author: Russ Allbery <[EMAIL PROTECTED]> > Date: Thu Jun 26 10:53:48 2008 -0700 > > Lower info-documents-not-removed to warning > > Unregistering info documents is a Policy should, not must.
Oops; thanks for fixing that. (Hurrah for overloading severity and certainty - as far as I can see all of the tags referring to Policy 12.2 refer to shoulds :-) Adam -- To UNSUBSCRIBE, email to [EMAIL PROTECTED] with a subject of "unsubscribe". Trouble? Contact [EMAIL PROTECTED]

