document w3cid property in editors list

see w3c/respec#398 (comment)
dontcallmedom · Feb 4, 2015 · 6653bb0 · 6653bb0
1 parent 978e761
commit 6653bb0
Showing 1 changed file with 5 additions and 0 deletions.
diff --git 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>