Skip to content
Snippets Groups Projects
Commit 401ad9be authored by Christoph Grüninger's avatar Christoph Grüninger
Browse files

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
parents b2d54827 d00519ce
No related branches found
No related tags found
No related merge requests found
Loading
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment