aboutsummaryrefslogtreecommitdiff
path: root/doc/manual.cli
diff options
context:
space:
mode:
authorKaren Arutyunov <karen@codesynthesis.com>2018-07-04 22:10:38 +0300
committerBoris Kolpackov <boris@codesynthesis.com>2018-07-05 08:49:59 +0200
commit9be433ac34057a2c9c1757ec41f8b3f6361f98dc (patch)
tree053bc111fd525086c29343195bea595eaca4d43b /doc/manual.cli
parentadefc9b14d8940299a0c6b478de8b66566978d10 (diff)
Strip .git extension for non-existent local prerequisite location
If the local prerequisite git repository having the .git extension doesn't exist but the one without the extension does, then strip the extension from the location.
Diffstat (limited to 'doc/manual.cli')
-rw-r--r--doc/manual.cli7
1 files changed, 6 insertions, 1 deletions
diff --git a/doc/manual.cli b/doc/manual.cli
index 16485df..5e2effe 100644
--- a/doc/manual.cli
+++ b/doc/manual.cli
@@ -1110,7 +1110,12 @@ already know the location of the base repository.} If the location is a
relative path, then it is treated as relative to the base repository location.
For the \cb{git} repository type the relative location does not inherit the
-URL fragment from the base repository.
+URL fragment from the base repository. Note also that the remote \cb{git}
+repository locations normally have the \cb{.git} extension that is stripped
+when a repository is cloned locally. To make the relative locations usable in
+both contexts, the \cb{.git} extension should be ignored if the local
+prerequisite repository with the extension does not exist while the one
+without the extension does.
For the \cb{dir} repository type the relative location may also contain the
URL fragment to make the same repository information usable in case the base