Merge branch 'feature/dunecontrol-git-worktree' into 'master'
make dunecontrol compatible with git worktrees
I currently have my dune directory where all the git repositories for the Dune modules reside with checked-out master branches.
To simplify testing the Dune 2.5 branches, I created a new dune-2.5 directory where I created linked worktrees for the releases/2.5 branch of each Dune module with git worktree
.
Unfortunately, dunecontrol
doesn't recognize these linked worktrees as git repositories. When I call e.g. dunecontrol update
it gives me warnings like
--- calling update for dune-common ---
WARNING: dune_common is not under a known version control system.
We support svn, git and cvs.
--- dune-common done ---
This is caused by the fact that dunecontrol
only checks whether .git exists as a directory, but in linked worktrees .git is a regular file containing the path of the main worktree.
This merge request fixes this problem by additionally checking if .git exists as a regular file.
See merge request !161 (merged)