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]

Reply via email to