From 9be433ac34057a2c9c1757ec41f8b3f6361f98dc Mon Sep 17 00:00:00 2001 From: Karen Arutyunov Date: Wed, 4 Jul 2018 22:10:38 +0300 Subject: 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. --- doc/manual.cli | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) (limited to 'doc') 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 -- cgit v1.1