diff options
| -rw-r--r-- | documentation/sdk-manual/sdk-extensible.xml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/documentation/sdk-manual/sdk-extensible.xml b/documentation/sdk-manual/sdk-extensible.xml index f941df33f5..07566c7923 100644 --- a/documentation/sdk-manual/sdk-extensible.xml +++ b/documentation/sdk-manual/sdk-extensible.xml @@ -236,7 +236,8 @@ and needs to be extracted to some local area - this time outside of the default workspace. - As always, if required <filename>devtool</filename> creates + If required, <filename>devtool</filename> + always creates a Git repository locally during the extraction. Furthermore, the first positional argument <replaceable>srctree</replaceable> in this case |