diff options
| author |  Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2016-10-06 18:54:21 +0200 |
|---|---|---|
| committer |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-10-12 13:47:34 +0200 |
| commit | 5232d2a29506ee30bf54336acf9998684a3b1cd9 (patch) | |
| tree | f4d97bc4d5d199c1949cc9e5a77108cc807be1c6 /configure.ml | |
| 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 'configure.ml')
| -rw-r--r-- | configure.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/configure.ml b/configure.ml index 23ec93e07..507fd351a 100644 --- a/configure.ml +++ b/configure.ml @@ -430,7 +430,7 @@ let dll = if os_type_win32 then ".dll" else ".so" let vcs = let git_dir = try Sys.getenv "GIT_DIR" with Not_found -> ".git" in - if dir_exists git_dir then "git" + if Sys.file_exists git_dir then "git" else if Sys.file_exists ".svn/entries" then "svn" else if dir_exists "{arch}" then "gnuarch" else "none" |