mirror of
https://github.com/Dev-Wiki/git-repo.git
synced 2025-09-26 18:42:14 +08:00
Support <remove-project name="X"> in manifest to remove/replace X
The manifest files now permit removing a project so the user can either keep it out of their client, or replace it with a different project using an entirely different configuration. Signed-off-by: Shawn O. Pearce <sop@google.com>
This commit is contained in:
@@ -22,6 +22,7 @@ following DTD:
|
||||
<!DOCTYPE manifest [
|
||||
<!ELEMENT manifest (remote*,
|
||||
default?,
|
||||
remove-project*,
|
||||
project*,
|
||||
add-remote*)>
|
||||
|
||||
@@ -47,6 +48,9 @@ following DTD:
|
||||
<!ATTLIST add-remote fetch CDATA #REQUIRED>
|
||||
<!ATTLIST add-remote review CDATA #IMPLIED>
|
||||
<!ATTLIST add-remote project-name CDATA #IMPLIED>
|
||||
|
||||
<!ELEMENT remove-project (EMPTY)>
|
||||
<!ATTLIST remove-project name CDATA #REQUIRED>
|
||||
]>
|
||||
|
||||
A description of the elements and their attributes follows.
|
||||
@@ -155,6 +159,18 @@ the majority of the project's object database to be obtained through
|
||||
these additional remotes.
|
||||
|
||||
|
||||
Element remove-project
|
||||
----------------------
|
||||
|
||||
Deletes the named project from the internal manifest table, possibly
|
||||
allowing a subsequent project element in the same manifest file to
|
||||
replace the project with a different source.
|
||||
|
||||
This element is mostly useful in the local_manifest.xml, where
|
||||
the user can remove a project, and possibly replace it with their
|
||||
own definition.
|
||||
|
||||
|
||||
Local Manifest
|
||||
==============
|
||||
|
||||
|
Reference in New Issue
Block a user