diff options
| author | Emilio Jesus Gallego Arias | 2018-10-02 16:26:18 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-10-03 13:18:33 +0200 |
| commit | fc75c8ebf556a0f95c9f42e864dbac73090ecc6a (patch) | |
| tree | 327c57309791e0606b6389c7482f6818a29c2d8d /configure.ml | |
| parent | 016f4a302090bcbb4ad47197dda2c60d6f598f6a (diff) | |
[dune] [opam] Install `revision` file when building with Dune.
Fixes #8621
Diffstat (limited to 'configure.ml')
| -rw-r--r-- | configure.ml | 15 |
1 files changed, 1 insertions, 14 deletions
diff --git a/configure.ml b/configure.ml index a508ac6071..7cc58a3506 100644 --- a/configure.ml +++ b/configure.ml @@ -525,22 +525,10 @@ let arch_is_win32 = (arch = "win32") let exe = exe := if arch_is_win32 then ".exe" else ""; !exe let dll = if os_type_win32 then ".dll" else ".so" -(** * VCS - - Is the source tree checked out from a recognised - Version Control System ? *) - -let vcs = - let git_dir = try Sys.getenv "GIT_DIR" with Not_found -> ".git" in - 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" - (** * Git Precommit Hook *) let _ = let f = ".git/hooks/pre-commit" in - if vcs = "git" && dir_exists ".git/hooks" && not (Sys.file_exists f) then begin + if dir_exists ".git/hooks" && not (Sys.file_exists f) then begin cprintf "Creating pre-commit hook in %s" f; let o = open_out f in let pr s = fprintf o s in @@ -1341,7 +1329,6 @@ let write_makefile f = pr "IDECDEPSFLAGS=%s\n" !idecdepsflags; pr "IDEINT=%s\n\n" !idearchdef; pr "# Defining REVISION\n"; - pr "CHECKEDOUT=%s\n\n" vcs; pr "# Option to control compilation and installation of the documentation\n"; pr "WITHDOC=%s\n\n" (if !prefs.withdoc then "all" else "no"); pr "# Option to produce precompiled files for native_compute\n"; |
