tree ef88b8c272ed2ce4e957c6ae10d52e142110ca32
parent 9cccf70b58828f84810c9de28e4a8c452b132309
author Václav Kubernát <kubernat@cesnet.cz> 1641374971 +0100
committer Václav Kubernát <kubernat@cesnet.cz> 1641375103 +0100

Make git repo detection cleverer

Currently, the script just checks whether we are inside a git
repository. However, in my setup, my home directory is a git repository
and that means that I have to run the script in an entirely different
place which is very annoying.

The new behavior is to check whether we are inside the same repository
as the dev-setup-git script.

Change-Id: I9072ad7a96f3521b470fd400d867c733a143b0d2