1 files changed, 4 insertions, 0 deletions

diff --git a/docs/manifest-format.md b/docs/manifest-format.md
index 45fd615e..c3bfcff0 100644
--- a/docs/manifest-format.md
+++ b/docs/manifest-format.md
@@ -96,6 +96,7 @@ following DTD:
 
   <!ELEMENT remove-project EMPTY>
   <!ATTLIST remove-project name  CDATA #REQUIRED>
+  <!ATTLIST remove-project optional  CDATA #IMPLIED>
 
   <!ELEMENT repo-hooks EMPTY>
   <!ATTLIST repo-hooks in-project CDATA #REQUIRED>
@@ -393,6 +394,9 @@ This element is mostly useful in a local manifest file, where
 the user can remove a project, and possibly replace it with their
 own definition.
 
+Attribute `optional`: Set to true to ignore remove-project elements with no
+matching `project` element.
+
 ### Element repo-hooks
 
 NB: See the [practical documentation](./repo-hooks.md) for using repo hooks.