From 6653bb0952d60df31945bc988c6d41b8af32a4f9 Mon Sep 17 00:00:00 2001
From: Dominique Hazael-Massieux <dom@w3.org>
Date: Wed, 4 Feb 2015 09:07:09 +0100
Subject: [PATCH] document w3cid property in editors list see
 https://github.com/w3c/respec/pull/398#issuecomment-72759084

---
 ref.html | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/ref.html b/ref.html
index 552ff64..d7430c0 100644
--- a/ref.html
+++ b/ref.html
@@ -156,6 +156,11 @@ <h2>editors</h2>
       switched companies during edition) or to clarify that an editor is no longer active even if her
       name is still attached to the document out of respect for her past contributions.
     </dd>
+    <dt>w3cid</dt>
+    <dd>
+      Numeric id of the editor profile in W3C; it is used by the
+      W3C publication system to associate specifications with their editors.
+    </dd>
   </dl>
 </section>