diff options
| author | Théo Zimmermann | 2016-10-06 18:54:21 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2016-10-12 13:47:34 +0200 |
| commit | 5232d2a29506ee30bf54336acf9998684a3b1cd9 (patch) | |
| tree | f4d97bc4d5d199c1949cc9e5a77108cc807be1c6 /dev | |
| parent | 55699e2b9a91356b7d43c4096f65fb199777b9a1 (diff) | |
Fix git recognition when in worktrees.
git worktrees have a .git file instead of a .git directory.
Using Sys.file_exists is a more general solution which gives true in both cases.
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions