diff options
| author | Karen Arutyunov <karen@codesynthesis.com> | 2018-07-04 22:10:38 +0300 |
|---|---|---|
| committer | Boris Kolpackov <boris@codesynthesis.com> | 2018-07-05 08:49:59 +0200 |
| commit | 9be433ac34057a2c9c1757ec41f8b3f6361f98dc (patch) | |
| tree | 053bc111fd525086c29343195bea595eaca4d43b /doc | |
| parent | adefc9b14d8940299a0c6b478de8b66566978d10 (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')
| -rw-r--r-- | doc/manual.cli | 7 |
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 |